show (maxInvFreeSet X).val ⊆ (maxInvFreeSet X).val.insert x⁻¹
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))) }
⊢ ↑(maxInvFreeSet X) ⊆ ↑C
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))) }
⊢ ↑(maxInvFreeSet X) ⊆ Set.insert x⁻¹ ↑(maxInvFreeSet X)