Assume H1 H2 H3 H4 H5.

We will prove (idT ∧ compT) ∧ (idL ∧ idR) ∧ compAssoc.

Apply and3I to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is H2.

Apply andI to the current goal.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is H4.

An exact proof term for the current goal is H5.

∎