exact (maxInvFreeSet X).prop x hx (hmem ▸ hx)
case pos
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∈ ↑(maxInvFreeSet X)
⊢ False
no goals