Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: x2 ∈ setexp x1 x0.

set y3 to be lam_comp x0 x2 (lam_id x0)

set y4 to be y3

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

Let x5 of type ι → ο be given.

Assume H1: x5 y4.

Apply encode_u_ext with x2, λ x6 . ap y4 (ap (lam_id x2) x6), λ x6 . ap y4 x6, λ x6 . x5 leaving 2 subgoals.

Let x6 of type ι be given.

Assume H2: x6 ∈ x2.

set y7 to be ap y4 (ap (lam x2 (λ x7 . x7)) x6)

set y8 to be ap x5 y7

Claim L3: ∀ x9 : ι → ο . x9 y8 ⟶ x9 y7

Let x9 of type ι → ο be given.

Assume H3: x9 (ap x6 y8).

set y10 to be λ x10 . x9

Apply beta with y4, λ x11 . x11, y8, λ x11 x12 . y10 (ap x6 x11) (ap x6 x12) leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

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

Apply L3 with λ x10 . x9 x10 y8 ⟶ x9 y8 x10.

Assume H4: x9 y8 y8.

The subproof is completed by applying H4.

Apply Pi_eta with x2, λ x6 . y3, y4, λ x6 . x5 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

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

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

Assume H2: x5 y4 y4.

The subproof is completed by applying H2.

■

Proofgold Proof