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: ∀ x4 . x4 ∈ x0 ⟶ x3 (ap x1 x4) (ap x2 x4).

Assume H1: ∀ x4 . x3 x4 x4.

Assume H2: ∀ x4 x5 . 3897e.. x0 x1 x2 x4 x5 ⟶ x3 x4 x5 ⟶ x3 x5 x4.

Assume H3: ∀ x4 x5 x6 . 3897e.. x0 x1 x2 x4 x5 ⟶ x3 x4 x5 ⟶ 3897e.. x0 x1 x2 x5 x6 ⟶ x3 x5 x6 ⟶ x3 x4 x6.

Claim L4: ∀ x4 x5 . 3897e.. x0 x1 x2 x4 x5 ⟶ and (3897e.. x0 x1 x2 x4 x5) (x3 x4 x5)

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H4: 3897e.. x0 x1 x2 x4 x5.

Apply H4 with λ x6 x7 . and (3897e.. x0 x1 x2 x6 x7) (x3 x6 x7) leaving 4 subgoals.

Let x6 of type ι be given.

Assume H5: x6 ∈ x0.

Apply andI with 3897e.. x0 x1 x2 (ap x1 x6) (ap x2 x6), x3 (ap x1 x6) (ap x2 x6) leaving 2 subgoals.

Apply unknownprop_4a9ee00be3059282c1c2c04c263a8ef11d5d96bde5e2cce739d1bcaa19845c62 with x0, x1, x2, x6.

The subproof is completed by applying H5.

Apply H0 with x6.

The subproof is completed by applying H5.

Let x6 of type ι be given.

Apply andI with 3897e.. x0 x1 x2 x6 x6, x3 x6 x6 leaving 2 subgoals.

The subproof is completed by applying unknownprop_f30a9971af522a7c6d48fce7503318aee70245a8fb07686f8a91c05461df8720 with x0, x1, x2, x6.

The subproof is completed by applying H1 with x6.

Let x6 of type ι be given.

Let x7 of type ι be given.

Assume H5: and (3897e.. x0 x1 x2 x6 x7) (x3 x6 x7).

Apply H5 with and (3897e.. x0 x1 x2 x7 x6) (x3 x7 x6).

Assume H6: 3897e.. x0 x1 x2 x6 x7.

Assume H7: x3 x6 x7.

Apply andI with 3897e.. x0 x1 x2 x7 x6, x3 x7 x6 leaving 2 subgoals.

Apply unknownprop_6fd31505fe5649eb2fd16580ea5d6e63ee118f3692b3972694e2469c77d587b4 with x0, x1, x2, x6, x7.

The subproof is completed by applying H6.

Apply H2 with x6, x7 leaving 2 subgoals.

The subproof is completed by applying H6.

The subproof is completed by applying H7.

Let x6 of type ι be given.

Let x7 of type ι be given.

Let x8 of type ι be given.

Assume H5: and (3897e.. x0 x1 x2 x6 x7) (x3 x6 x7).

Assume H6: and (3897e.. x0 x1 x2 x7 x8) (x3 x7 x8).

Apply H5 with and (3897e.. x0 x1 x2 x6 x8) (x3 x6 x8).

Assume H7: 3897e.. x0 x1 x2 x6 x7.

Assume H8: x3 x6 x7.

Apply H6 with and (3897e.. x0 x1 x2 x6 ...) ....

...

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H5: 3897e.. x0 x1 x2 x4 x5.

Apply L4 with x4, x5, x3 x4 x5 leaving 2 subgoals.

The subproof is completed by applying H5.

Assume H6: 3897e.. x0 x1 x2 x4 x5.

Assume H7: x3 x4 x5.

The subproof is completed by applying H7.

■

Proofgold Proof