Let x0 of type ι be given.
Apply encode_u_ext with
omega,
λ x1 . ap x0 (ordsucc x1),
λ x1 . ap (lam omega (λ x2 . ap x0 (ordsucc x2))) x1.
Let x1 of type ι be given.
Let x2 of type ι → ι → ο be given.
Apply beta with
omega,
λ x3 . ap x0 (ordsucc x3),
x1,
λ x3 x4 . x2 x4 x3.
The subproof is completed by applying H0.