Let x0 of type ι be given.
Apply HSNo_E with
x0,
λ x1 . ordinal (HSNoLev x1) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply HSNo_proj0_2 with
x1,
x2,
λ x3 x4 . ordinal (binunion (CSNoLev x4) (CSNoLev (HSNo_proj1 (CSNo_pair x1 x2)))) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply HSNo_proj1_2 with
x1,
x2,
λ x3 x4 . ordinal (binunion (CSNoLev x1) (CSNoLev x4)) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply ordinal_binunion with
CSNoLev x1,
CSNoLev x2 leaving 2 subgoals.
Apply CSNoLev_ordinal with
x1.
The subproof is completed by applying H1.
Apply CSNoLev_ordinal with
x2.
The subproof is completed by applying H2.