Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: x2 ∈ setexp x1 x0.

Let x3 of type ι be given.

Let x4 of type ι be given.

Apply encode_u_ext with x0, λ x5 . ap x4 (ap (lam_comp x0 x3 x2) x5), λ x5 . ap (lam_comp x1 x4 x3) (ap x2 x5).

Let x5 of type ι be given.

Assume H1: x5 ∈ x0.

set y6 to be ap x4 (ap (lam_comp x0 x3 x2) x5)

set y7 to be ap (lam_comp x2 x5 x4) (ap x3 y6)

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

Let x8 of type ι → ο be given.

Assume H2: x8 (ap (lam_comp x3 y6 x5) (ap x4 y7)).

set y9 to be ap y6 (ap (lam_comp x2 x5 x4) y7)

set y10 to be ap y7 (ap y6 (ap x5 x8))

Claim L3: ∀ x11 : ι → ο . x11 y10 ⟶ x11 y9

Let x11 of type ι → ο be given.

Assume H3: x11 (ap x8 (ap y7 (ap y6 y9))).

set y12 to be λ x12 . x11

Apply beta with x4, λ x13 . ap y7 (ap y6 x13), y9, λ x13 x14 . y12 (ap x8 x13) (ap x8 x14) leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

set y11 to be λ x11 . y10

Apply L3 with λ x12 . y11 x12 y10 ⟶ y11 y10 x12 leaving 2 subgoals.

Assume H4: y11 y10 y10.

The subproof is completed by applying H4.

set y12 to be λ x12 . y11

Apply beta with y6, λ x13 . ap y9 (ap x8 x13), ap y7 y10, λ x13 x14 . y12 x14 x13 leaving 2 subgoals.

Apply ap_Pi with x5, λ x13 . y6, y7, y10 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

The subproof is completed by applying L3.

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

Apply L2 with λ x9 . x8 x9 y7 ⟶ x8 y7 x9.

Assume H3: x8 y7 y7.

The subproof is completed by applying H3.

■

Proofgold Proof