Let X and s be given.
Assume HsSubX.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ intersection_of_family X {s}.
We will prove x ∈ s.
We prove the intermediate claim Hall: ∀U : set, U ∈ {s} → x ∈ U.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U : set, U ∈ {s} → x0 ∈ U) x Hx).
An exact proof term for the current goal is (Hall s (SingI s)).
Let x be given.
Assume Hx: x ∈ s.
We will prove x ∈ intersection_of_family X {s}.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HsSubX x Hx).
We prove the intermediate claim Hprop: ∀U : set, U ∈ {s} → x ∈ U.
Let U be given.
Assume HU: U ∈ {s}.
We will prove x ∈ U.
We prove the intermediate claim HUeq: U = s.
An exact proof term for the current goal is (SingE s U HU).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∀U : set, U ∈ {s} → x0 ∈ U) x HxX Hprop).
∎