subst ‹a = x⁻¹›
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a = x⁻¹
⊢ a⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ x⁻¹⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}