Let A, B, C, D and E be given.

Assume H.

Let p be given.

Assume Hp.

Apply (H p) to the current goal.

Assume H1 He.

Apply (H1 p) to the current goal.

Assume H2 Hd.

Apply (H2 p) to the current goal.

Assume H3 Hc.

Apply (H3 p) to the current goal.

Assume Ha Hb.

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

∎