Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: x1 = lam omega (λ x2 . ap x1 x2).

set y2 to be stream_rest (4ec03.. x0 x1)

set y3 to be y2

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

Let x4 of type ι → ο be given.

Assume H1: x4 y3.

Apply encode_u_ext with omega, λ x5 . ap (4ec03.. y2 y3) (ordsucc x5), λ x5 . ap y3 x5, λ x5 . x4 leaving 2 subgoals.

Let x5 of type ι be given.

Assume H2: x5 ∈ omega.

Apply unknownprop_4270b0e920f6ab49c5577490ca19e4c5c6282a2ea155f48817cbf066c86da489 with y2, y3, x5.

The subproof is completed by applying H2.

set y5 to be λ x5 . x4

Apply H0 with λ x6 x7 . y5 x7 x6.

The subproof is completed by applying H1.

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

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

Assume H2: x4 y3 y3.

The subproof is completed by applying H2.

■

Proofgold Proof