dsimp [orientation]
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ orientation x ≠ orientation x⁻¹
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ ¬decide (x ∈ ↑(maxInvFreeSet X)) = decide (x⁻¹ ∈ ↑(maxInvFreeSet X))