Theorem star_inv₀

Modification history