Let A, B, C and D be given.

Assume H.

Let p be given.

Assume Hp.

Apply (H p) to the current goal.

Assume H1 Hd.

Apply (H1 p) to the current goal.

Assume H2 Hc.

Apply (H2 p) to the current goal.

Assume Ha Hb.

An exact proof term for the current goal is (Hp Ha Hb Hc Hd).

∎