Let X, x, y and p be given.

Assume Hfun: function_on p unit_interval X.

Assume H0: apply_fun p 0 = x.

Assume H1: apply_fun p 1 = y.

We prove the intermediate claim Hpair0: function_on p unit_interval X ∧ apply_fun p 0 = x.

An exact proof term for the current goal is (andI (function_on p unit_interval X) (apply_fun p 0 = x) Hfun H0).

An exact proof term for the current goal is (andI (function_on p unit_interval X ∧ apply_fun p 0 = x) (apply_fun p 1 = y) Hpair0 H1).

∎