Let X, x, y and p be given.

Assume H: path_between X x y p.

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

∎