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

Assume H.

Let p be given.

Assume Hp.

Apply (H p) to the current goal.

Assume H1 Hf.

Apply (H1 p) to the current goal.

Assume H2 He.

Apply (H2 p) to the current goal.

Assume H3 Hd.

Apply (H3 p) to the current goal.

Assume H4 Hc.

Apply (H4 p) to the current goal.

Assume Ha Hb.

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

∎