Proofgold Proof

pf

Let x0 of type ι → ι → ο be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: 8e91b.. x0 x1 x2.

Assume H1: 8e91b.. x0 x2 x3.

Let x4 of type ι → ι → ο be given.

Assume H2: ∀ x5 x6 . x0 x5 x6 ⟶ x4 x5 x6.

Assume H3: ∀ x5 x6 x7 . x4 x5 x6 ⟶ x4 x6 x7 ⟶ x4 x5 x7.

Apply H3 with x1, x2, x3 leaving 2 subgoals.

Apply H0 with x4 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

Apply H1 with x4 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

■