Let X, Fam and x be given.

Assume HxX: x ∈ X.

Assume Hall: ∀U : set, U ∈ Fam → x ∈ U.

An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∀U : set, U ∈ Fam → x0 ∈ U) x HxX Hall).

∎