Let X, Fam and x be given.
Assume Hx: x ∈ intersection_of_family X Fam.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U : set, U ∈ Fam → x0 ∈ U) x Hx).
∎