Let A, Y and f be given.
Assume Hdom: graph_domain_subset f A.
Assume Htot: total_function_on f A Y.
Assume Hfun: functional_graph f.
Let x and y be given.
Assume Hxy: (x,y) ∈ f.
We will prove y ∈ Y.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (Hdom x y Hxy).
We prove the intermediate claim HappY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y f A Y x Htot HxA).
We prove the intermediate claim HappEq: apply_fun f x = y.
An exact proof term for the current goal is (functional_graph_apply_fun_eq f x y Hfun Hxy).
rewrite the current goal using HappEq (from right to left).
An exact proof term for the current goal is HappY.
∎