Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: 80242.. x0.

Assume H1: 80242.. x1.

Assume H2: 80242.. x2.

set y3 to be f4dc0.. (bc82c.. x0 (bc82c.. x1 x2))

set y4 to be bc82c.. (f4dc0.. x1) (bc82c.. (f4dc0.. x2) (f4dc0.. y3))

Claim L3: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3

Let x5 of type ι → ο be given.

Assume H3: x5 (bc82c.. (f4dc0.. x2) (bc82c.. (f4dc0.. y3) (f4dc0.. y4))).

Apply unknownprop_0d56d2036eb40449eff19abcb7d6bdbc877769b25cd503ef42fbe3121a69ddde with x2, bc82c.. y3 y4, λ x6 . x5 leaving 3 subgoals.

The subproof is completed by applying H0.

Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with y3, y4 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

set y6 to be bc82c.. (f4dc0.. x2) (f4dc0.. (bc82c.. y3 y4))

set y7 to be bc82c.. (f4dc0.. y3) (bc82c.. (f4dc0.. y4) (f4dc0.. x5))

Claim L4: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6

Let x8 of type ι → ο be given.

Assume H4: x8 (bc82c.. (f4dc0.. y4) (bc82c.. (f4dc0.. x5) (f4dc0.. y6))).

set y9 to be λ x9 . x8

Apply unknownprop_0d56d2036eb40449eff19abcb7d6bdbc877769b25cd503ef42fbe3121a69ddde with x5, y6, λ x10 x11 . y9 (bc82c.. (f4dc0.. y4) x10) (bc82c.. (f4dc0.. y4) x11) leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

The subproof is completed by applying H4.

set y8 to be λ x8 . y7

Apply L4 with λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.

Assume H5: y8 y7 y7.

The subproof is completed by applying H5.

The subproof is completed by applying L4.

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

Apply L3 with λ x6 . x5 x6 y4 ⟶ x5 y4 x6.

Assume H4: x5 y4 y4.

The subproof is completed by applying H4.

■

Proofgold Proof