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

Assume H.

Let p be given.

Assume Hp.

Apply (H p) to the current goal.

Assume H1 Hg.

Apply (H1 p) to the current goal.

Assume H2 Hf.

Apply (H2 p) to the current goal.

Assume H3 He.

Apply (H3 p) to the current goal.

Assume H4 Hd.

Apply (H4 p) to the current goal.

Assume H5 Hc.

Apply (H5 p) to the current goal.

Assume Ha Hb.

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

∎