simp [not_or]
case inr
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
⊢ a⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
case inr
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
⊢ ¬a = x ∧ a⁻¹ ∉ ↑(maxInvFreeSet X)