Let x0 of type ι be given.
Let x1 of type ι be given.
Apply SNo_SNo with
x1,
binintersect x0 (SNoElts_ x1).
Apply ordinal_Hered with
SNoLev x0,
x1 leaving 2 subgoals.
Apply SNoLev_ordinal with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.