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.
Assume H10: P10.
Assume H11: P11.
Assume H12: P12.
Assume H13: P13.
Assume H14: P14.
Apply andI to the current goal.
We will prove P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 ∧ P8 ∧ P9 ∧ P10 ∧ P11 ∧ P12 ∧ P13.
Apply and13I 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.
An exact proof term for the current goal is H10.
An exact proof term for the current goal is H11.
An exact proof term for the current goal is H12.
An exact proof term for the current goal is H13.
An exact proof term for the current goal is H14.
∎