Let X, Tx, Y, Ty and f be given.

Assume H: embedding_of X Tx Y Ty f.

We prove the intermediate claim HdefEmb: embedding_of X Tx Y Ty f = (continuous_map X Tx Y Ty f ∧ homeomorphism X Tx (image_of f X) (subspace_topology Y Ty (image_of f X)) f).

Use reflexivity.

We prove the intermediate claim Hpair: continuous_map X Tx Y Ty f ∧ homeomorphism X Tx (image_of f X) (subspace_topology Y Ty (image_of f X)) f.

rewrite the current goal using HdefEmb (from right to left).

An exact proof term for the current goal is H.

An exact proof term for the current goal is (andEL (continuous_map X Tx Y Ty f) (homeomorphism X Tx (image_of f X) (subspace_topology Y Ty (image_of f X)) f) Hpair).

∎