Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι be given.
Assume H1:
∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ x1 x3 = x2 x3.
Apply nat_ind with
λ x3 . SNo_sqrtaux x0 x1 x3 = SNo_sqrtaux x0 x2 x3 leaving 2 subgoals.
Apply SNo_sqrtaux_0 with
x0,
x1,
λ x3 x4 . x4 = SNo_sqrtaux x0 x2 0.
Apply SNo_sqrtaux_0 with
x0,
x2,
λ x3 x4 . lam 2 (λ x5 . If_i (x5 = 0) (prim5 (SNoL_nonneg x0) x1) (prim5 (SNoR x0) x1)) = x4.
Apply ReplEq_ext with
SNoL_nonneg x0,
x1,
x2,
λ x3 x4 . lam 2 (λ x5 . If_i (x5 = 0) x4 {x1 x6|x6 ∈ SNoR x0}) = lam 2 (λ x5 . If_i (x5 = 0) {x2 x6|x6 ∈ SNoL_nonneg x0} {x2 x6|x6 ∈ SNoR x0}) leaving 2 subgoals.
Let x3 of type ι be given.
Apply SNoL_E with
x0,
x3,
x1 x3 = x2 x3 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply SepE1 with
SNoL x0,
λ x4 . SNoLe 0 x4,
x3.
The subproof is completed by applying H2.
Apply H1 with
x3.
Apply SNoS_I2 with
x3,
x0 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply ReplEq_ext with
SNoR x0,
x1,
x2,
λ x3 x4 . lam 2 (λ x5 . If_i (x5 = 0) {x2 x6|x6 ∈ SNoL_nonneg x0} x4) = lam 2 (λ x5 . If_i (x5 = 0) {x2 x6|x6 ∈ SNoL_nonneg x0} {x2 x6|x6 ∈ SNoR x0}) leaving 2 subgoals.
Let x3 of type ι be given.
Apply SNoR_E with
x0,
x3,
x1 x3 = x2 x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply H1 with
x3.
Apply SNoS_I2 with
x3,
x0 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Let x4 of type ι → ι → ο be given.
Assume H2: x4 y3 y3.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Apply SNo_sqrtaux_S with
x0,
x1,
x3,
λ x4 x5 . x5 = SNo_sqrtaux x0 x2 (ordsucc x3) leaving 2 subgoals.
The subproof is completed by applying H2.