An exact proof term for the current goal is (andEL (function_on f X Y) (∀x : set, x ∈ X → ∃y : set, y ∈ Y ∧ (x,y) ∈ f) H).