Let f, X, Y and x be given.

Assume Htot: total_function_on f X Y.

Assume HxX: x ∈ X.

We prove the intermediate claim Hfun: function_on f X Y.

An exact proof term for the current goal is (total_function_on_function_on f X Y Htot).

An exact proof term for the current goal is (Hfun x HxX).

∎