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

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

Assume H0: ∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 x3.

Assume H1: ∀ x2 . x1 x2 x2.

Assume H2: ∀ x2 x3 . 43cf7.. x0 x2 x3 ⟶ x1 x2 x3 ⟶ x1 x3 x2.

Assume H3: ∀ x2 x3 x4 . 43cf7.. x0 x2 x3 ⟶ x1 x2 x3 ⟶ 43cf7.. x0 x3 x4 ⟶ x1 x3 x4 ⟶ x1 x2 x4.

Claim L4: ∀ x2 x3 . 43cf7.. x0 x2 x3 ⟶ and (43cf7.. x0 x2 x3) (x1 x2 x3)

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H4: 43cf7.. x0 x2 x3.

Apply H4 with λ x4 x5 . and (43cf7.. x0 x4 x5) (x1 x4 x5) leaving 4 subgoals.

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H5: x0 x4 x5.

Apply andI with 43cf7.. x0 x4 x5, x1 x4 x5 leaving 2 subgoals.

Apply unknownprop_f0c6a23e8b8f78c08ee5fe27237fc8b3f56d1599a38a3401bced9c42269fcbe4 with x0, x4, x5.

The subproof is completed by applying H5.

Apply H0 with x4, x5.

The subproof is completed by applying H5.

Let x4 of type ι be given.

Apply andI with 43cf7.. x0 x4 x4, x1 x4 x4 leaving 2 subgoals.

The subproof is completed by applying unknownprop_29cfbf8a9c6eed014dba54148f0cd09cea17c54902b9660d408603b8b7dcd3ba with x0, x4.

The subproof is completed by applying H1 with x4.

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H5: and (43cf7.. x0 x4 x5) (x1 x4 x5).

Apply H5 with and (43cf7.. x0 x5 x4) (x1 x5 x4).

Assume H6: 43cf7.. x0 x4 x5.

Assume H7: x1 x4 x5.

Apply andI with 43cf7.. x0 x5 x4, x1 x5 x4 leaving 2 subgoals.

Apply unknownprop_7047b95e6173122a3abb1a32266f1489e266d3c8ab3b5c6967895c784d08d3b9 with x0, x4, x5.

The subproof is completed by applying H6.

Apply H2 with x4, x5 leaving 2 subgoals.

The subproof is completed by applying H6.

The subproof is completed by applying H7.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H5: and (43cf7.. x0 x4 x5) (x1 x4 x5).

Assume H6: and (43cf7.. x0 x5 x6) (x1 x5 x6).

Apply H5 with and (43cf7.. x0 x4 x6) (x1 x4 x6).

Assume H7: 43cf7.. x0 x4 x5.

Assume H8: x1 x4 x5.

Apply H6 with and (43cf7.. x0 x4 x6) (x1 x4 x6).

Assume H9: 43cf7.. x0 x5 x6.

Assume H10: x1 x5 x6.

Apply andI with 43cf7.. x0 x4 x6, x1 x4 x6 leaving 2 subgoals.

Apply unknownprop_b4019bc0970596b58612a8ffb42269b10648c70776df5ab173906cbf3999bbc4 with x0, x4, x5, x6 leaving 2 subgoals.

The subproof is completed by applying H7.

The subproof is completed by applying H9.

Apply H3 with x4, x5, x6 leaving 4 subgoals.

The subproof is completed by applying H7.

The subproof is completed by applying H8.

The subproof is completed by applying H9.

The subproof is completed by applying H10.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H5: 43cf7.. x0 x2 x3.

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

The subproof is completed by applying H5.

Assume H6: 43cf7.. x0 x2 x3.

Assume H7: x1 x2 x3.

The subproof is completed by applying H7.

■

Proofgold Proof