simp
case h.h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
x✝ : X
⊢ x✝ ∈ ⋃ i, ⋃ (_ : i ∈ c ∧ ↑i = ↑A), ↑A ↔ x✝ ∈ ↑A
case h.h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
x✝ : X
⊢ x✝ ∈ ↑A → InvFreeSet ↑A ∧ A ∈ c