Let x0 of type ι be given.
Apply sqrt_SNo_nonneg_0 with
λ x1 x2 . x1 ∈ (λ x3 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x3) 0) 0.
Apply SNo_sqrtaux_0 with
x0,
sqrt_SNo_nonneg,
λ x1 x2 . sqrt_SNo_nonneg 0 ∈ ap x2 0.
Apply tuple_2_0_eq with
prim5 (SNoL_nonneg x0) sqrt_SNo_nonneg,
prim5 (SNoR x0) sqrt_SNo_nonneg,
λ x1 x2 . sqrt_SNo_nonneg 0 ∈ x2.
Apply ReplI with
SNoL_nonneg x0,
sqrt_SNo_nonneg,
0.
Apply SepI with
SNoL x0,
λ x1 . SNoLe 0 x1,
0 leaving 2 subgoals.
Apply SNoL_I with
x0,
0 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
Apply SNoLev_0 with
λ x1 x2 . x2 ∈ SNoLev x0.
The subproof is completed by applying H2.
Apply SNoLeE with
0,
x0,
SNoLt 0 x0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Assume H3: 0 = x0.
Apply FalseE with
SNoLt 0 x0.
Apply EmptyE with
0.
Apply SNoLev_0 with
λ x1 x2 . 0 ∈ x1.
Apply H3 with
λ x1 x2 . 0 ∈ SNoLev x2.
The subproof is completed by applying H2.
The subproof is completed by applying SNoLe_ref with 0.