rw [@decide_eq_decide]
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ ¬decide (x ∈ ↑(maxInvFreeSet X)) = decide (x⁻¹ ∈ ↑(maxInvFreeSet X))
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ ¬(x ∈ ↑(maxInvFreeSet X) ↔ x⁻¹ ∈ ↑(maxInvFreeSet X))