Let x0 of type ι be given.
Apply CSNo_E with
x0,
λ x1 . ordinal (CSNoLev x1) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply CSNo_Re2 with
x1,
x2,
λ x3 x4 . ordinal (binunion (SNoLev x4) (SNoLev (CSNo_Im (SNo_pair x1 x2)))) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply CSNo_Im2 with
x1,
x2,
λ x3 x4 . ordinal (binunion (SNoLev x1) (SNoLev x4)) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply ordinal_binunion with
SNoLev x1,
SNoLev x2 leaving 2 subgoals.
Apply SNoLev_ordinal with
x1.
The subproof is completed by applying H1.
Apply SNoLev_ordinal with
x2.
The subproof is completed by applying H2.