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