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