Assume H1: P1.
Assume H2: P2.
Assume H3: P3.
Assume H4: P4.
Assume H5: P5.
Assume H6: P6.
Assume H7: P7.
Assume H8: P8.
Assume H9: P9.
Apply andI to the current goal.
We will prove P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 ∧ P8.
Apply and8I to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H2.
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.
An exact proof term for the current goal is H6.
An exact proof term for the current goal is H7.
An exact proof term for the current goal is H8.
An exact proof term for the current goal is H9.
∎