aesop (add norm simp [Set.insert])
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
a✝ : X
⊢ a✝ ∈ ↑(maxInvFreeSet X) → a✝ ∈ Set.insert x⁻¹ ↑(maxInvFreeSet X)
no goals