Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: c7ce4.. x0.

Assume H1: c7ce4.. x1.

Assume H2: 28f8d.. x0 = 28f8d.. x1.

Assume H3: d634d.. x0 = d634d.. 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_5b83866c440783e0b1a158e0891e967d7f7864776be8302794e7cb2317ac7efc with y2, λ x5 . x4 leaving 2 subgoals.

The subproof is completed by applying H0.

set y5 to be ad280.. (28f8d.. y2) (d634d.. 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 . ad280.. x9 (d634d.. x4) = ad280.. (28f8d.. y5) (d634d.. y5), λ x8 . x7 leaving 2 subgoals.

Apply H3 with λ x8 x9 . ad280.. (28f8d.. y5) x9 = ad280.. (28f8d.. y5) (d634d.. y5).

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

Assume H6: x8 (ad280.. (28f8d.. y5) (d634d.. y5)) (ad280.. (28f8d.. y5) (d634d.. y5)).

The subproof is completed by applying H6.

set y8 to be λ x8 . x7

Apply unknownprop_5b83866c440783e0b1a158e0891e967d7f7864776be8302794e7cb2317ac7efc 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