intro hmem
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ ¬(x ∈ ↑(maxInvFreeSet X) ↔ x⁻¹ ∈ ↑(maxInvFreeSet X))
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : x ∈ ↑(maxInvFreeSet X) ↔ x⁻¹ ∈ ↑(maxInvFreeSet X)
⊢ False