Let X, Tx, x, y and p be given.

Assume H: path_between X x y p ∧ continuous_map unit_interval unit_interval_topology X Tx p.

An exact proof term for the current goal is (andEL (path_between X x y p) (continuous_map unit_interval unit_interval_topology X Tx p) H).

∎