Let f, X, X' and Y be given.

Assume Hfun: function_on f X Y.

Assume Hsub: X' ⊆ X.

Let x be given.

Assume HxX': x ∈ X'.

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

∎