Let X, Y and f be given.

Assume Hf.

Let p be given.

Assume Hp.

Apply Hf to the current goal.

Assume Hf.

Apply Hf to the current goal.

Assume Hf1 Hf2 Hf3.

An exact proof term for the current goal is Hp Hf1 Hf2 Hf3.

∎