rw [@iff_eq_eq] at hmem
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : x ∈ ↑(maxInvFreeSet X) ↔ x⁻¹ ∈ ↑(maxInvFreeSet X)
⊢ False
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
⊢ False