Let x0 of type ι be given.
Apply add_SNo_0L with
x0,
λ x1 x2 . ordsucc x1 = add_SNo 1 x0 leaving 2 subgoals.
Apply ordinal_SNo with
x0.
The subproof is completed by applying H0.
Let x1 of type ι → ι → ο be given.
Apply add_SNo_ordinal_SL with
0,
x0,
λ x2 x3 . x1 x3 x2 leaving 2 subgoals.
The subproof is completed by applying ordinal_Empty.
The subproof is completed by applying H0.