Let X, x, y and p be given.

Assume H: path_between X x y p.

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

An exact proof term for the current goal is (path_between_pair0 X x y p H).

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

∎