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 x0 (λ x3 . ap (lam_id x1) (ap x2 x3))

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 (lam_id y3) (ap y4 x6), λ x6 . ap y4 x6, λ x6 . x5 leaving 2 subgoals.

Let x6 of type ι be given.

Assume H2: x6 ∈ x2.

Apply beta with y3, λ x7 . x7, ap y4 x6.

Apply ap_Pi with x2, λ x7 . y3, y4, x6 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H2.

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