Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: 1013b.. x0.

Assume H1: 1013b.. x1.

Assume H2: ce322.. x0 = ce322.. x1.

Assume H3: f6a32.. x0 = f6a32.. x1.

set y2 to be x0

set y3 to be y2

Claim L4: ∀ x4 : ι → ο . x4 y3 ⟶ x4 y2

Let x4 of type ι → ο be given.

Assume H4: x4 y3.

Apply unknownprop_5bfa7e2c4e0c8770e52c317d4111804765880efbe213ccc7f49552da8205fc8a with y2, λ x5 . x4 leaving 2 subgoals.

The subproof is completed by applying H0.

set y5 to be 236dc.. (ce322.. y2) (f6a32.. y2)

set y6 to be x4

Claim L5: ∀ x7 : ι → ο . x7 y6 ⟶ x7 y5

Let x7 of type ι → ο be given.

Assume H5: x7 y5.

Apply H2 with λ x8 x9 . 236dc.. x9 (f6a32.. x4) = 236dc.. (ce322.. y5) (f6a32.. y5), λ x8 . x7 leaving 2 subgoals.

Apply H3 with λ x8 x9 . 236dc.. (ce322.. y5) x9 = 236dc.. (ce322.. y5) (f6a32.. y5).

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

Assume H6: x8 (236dc.. (ce322.. y5) (f6a32.. y5)) (236dc.. (ce322.. y5) (f6a32.. y5)).

The subproof is completed by applying H6.

set y8 to be λ x8 . x7

Apply unknownprop_5bfa7e2c4e0c8770e52c317d4111804765880efbe213ccc7f49552da8205fc8a with y5, λ x9 x10 . y8 x10 x9 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H5.

set y7 to be λ x7 . y6

Apply L5 with λ x8 . y7 x8 y6 ⟶ y7 y6 x8 leaving 2 subgoals.

Assume H6: y7 y6 y6.

The subproof is completed by applying H6.

The subproof is completed by applying L5.

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

Apply L4 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.

Assume H5: x4 y3 y3.

The subproof is completed by applying H5.

■

Proofgold Proof