simp only [Set.mem_setOf_eq] at h
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h✝ : x ∉ ↑(maxInvFreeSet X)
a : X
h : a ∈ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
⊢ a⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h✝ : x ∉ ↑(maxInvFreeSet X)
a : X
h : a = x⁻¹ ∨ a ∈ ↑(maxInvFreeSet X)
⊢ a⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}