Let z be given.

Assume Hz.

Let p be given.

Assume Hp.

Apply Hz to the current goal.

Let x be given.

Assume H1.

Apply H1 to the current goal.

Assume Hx.

Assume H1.

Apply H1 to the current goal.

Let y be given.

Assume H1.

Apply H1 to the current goal.

Assume Hy Hzxy.

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

An exact proof term for the current goal is Hp x y Hx Hy Hzxy.

∎