Assume HC.

Let p be given.

Assume Hp.

Apply HC to the current goal.

Assume H14 H5.

Apply H14 to the current goal.

Assume H12 H34.

Apply H12 to the current goal.

Assume H1 H2.

Apply H34 to the current goal.

Assume H3 H4.

An exact proof term for the current goal is Hp H1 H2 H3 H4 H5.

∎