Let x0 of type ι be given.
Apply SNo_extend1_SNo with
x0.
The subproof is completed by applying H0.
Apply SNo_extend1_SNoLev with
x0,
λ x1 x2 . SNoLev x0 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying ordsuccI2 with
SNoLev x0.
Apply SNo_eq with
x0,
binintersect (SNo_extend1 x0) (SNoElts_ (SNoLev x0)) leaving 4 subgoals.
The subproof is completed by applying H0.
Apply restr_SNo with
SNo_extend1 x0,
SNoLev x0 leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Let x1 of type ι → ι → ο be given.
Apply restr_SNoLev with
SNo_extend1 x0,
SNoLev x0,
λ x2 x3 . x1 x3 x2 leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.