Let f, X, Y and x be given.
Assume Htot: total_function_on f X Y.
Assume Hdom: graph_domain_subset f X.
Apply iffI to the current goal.
Assume HxX: x ∈ X.
We prove the intermediate claim Hex: ∃y : set, y ∈ Y ∧ (x,y) ∈ f.
An exact proof term for the current goal is (total_function_on_totality f X Y Htot x HxX).
Apply Hex to the current goal.
Let y be given.
Assume Hy: y ∈ Y ∧ (x,y) ∈ f.
We use y to witness the existential quantifier.
An exact proof term for the current goal is (andER (y ∈ Y) ((x,y) ∈ f) Hy).
Assume Hex: ∃y : set, (x,y) ∈ f.
Apply Hex to the current goal.
Let y be given.
Assume Hxy: (x,y) ∈ f.
An exact proof term for the current goal is (Hdom x y Hxy).
∎