Let x0 of type ι be given.
Apply EmptyE with
sqrt_SNo_nonneg 0.
Apply H3 with
λ x1 x2 . sqrt_SNo_nonneg 0 ∈ x1.
Apply famunionI with
omega,
λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0,
0,
sqrt_SNo_nonneg 0 leaving 2 subgoals.
Apply nat_p_omega with
0.
The subproof is completed by applying nat_0.
Apply sqrt_SNo_nonneg_0 with
λ x1 x2 . x2 ∈ (λ x3 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x3) 0) 0.
Apply sqrt_SNo_nonneg_0inL0 with
x0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.