An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ Rlt (apply_fun d (x,y0)) r) y Hy).