Let X, d, x, r and y be given.

Assume HyX: y ∈ X.

Assume Hlt: Rlt (apply_fun d (x,y)) r.

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

∎