Let x0 of type ι be given.
Apply unknownprop_c48a26f735e8c3ab42bca248200ba77259f8736379600b6a02793210bf5e2242 with
x0,
and (ordinal (SNoLev x0)) (SNo_ (SNoLev x0) x0) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Apply unknownprop_1aaa3a3361ce5ca6cf2b6994e7a734890eb3d044824fcd04645684b413a74dfd with
λ x2 x3 : ι → ι . and (ordinal (x3 x0)) (SNo_ (x3 x0) x0).
Apply unknownprop_c3f0de4cb966012957ca752938aa96a32c594389e7aea45227d571c0506618ba with
λ x2 . and (ordinal x2) (SNo_ x2 x0),
x1.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
ordinal x1,
SNo_ x1 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.