Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply encode_u_ext with
omega,
λ x4 . ap x1 x4,
λ x4 . ap x3 x4.
Let x4 of type ι be given.
Apply unknownprop_4270b0e920f6ab49c5577490ca19e4c5c6282a2ea155f48817cbf066c86da489 with
x0,
x1,
x4,
λ x5 x6 . x5 = ap x3 x4 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_4270b0e920f6ab49c5577490ca19e4c5c6282a2ea155f48817cbf066c86da489 with
x2,
x3,
x4,
λ x5 x6 . ap (4ec03.. x0 x1) (ordsucc x4) = x5 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply H0 with
λ x5 x6 . ap x6 (ordsucc x4) = ap (4ec03.. x2 x3) (ordsucc x4).
Let x5 of type ι → ι → ο be given.
The subproof is completed by applying H2.