Let P and Q be given.

Assume H.

Let p be given.

Assume Hp.

Apply H to the current goal.

Let x be given.

Assume H0.

Apply H0 to the current goal.

Assume H1 H2.

An exact proof term for the current goal is Hp x H1 H2.

∎