Let f, x and y be given.
Assume Hfun: functional_graph f.
Assume Hxy: (x,y) ∈ f.
We prove the intermediate claim Happ: (x,apply_fun f x) ∈ f.
An exact proof term for the current goal is (Eps_i_ax (λy0 : set ⇒ (x,y0) ∈ f) y Hxy).
An exact proof term for the current goal is (Hfun x (apply_fun f x) y Happ Hxy).
∎