Let x be given.
Assume Hx Hxnn H1.
Set L_ to be the term λk : set ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 0.
We will prove 0 ∈ L_ 0.
rewrite the current goal using sqrt_SNo_nonneg_0 (from right to left) at position 1.
We will prove sqrt_SNo_nonneg 0 ∈ SNo_sqrtaux x sqrt_SNo_nonneg 0 0.
rewrite the current goal using SNo_sqrtaux_0 x sqrt_SNo_nonneg (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove sqrt_SNo_nonneg 0 ∈ {sqrt_SNo_nonneg w|w ∈ SNoL_nonneg x}.
Apply ReplI to the current goal.
We will prove 0 ∈ SNoL_nonneg x.
We will prove 0 ∈ {w ∈ SNoL x|0 ≤ w}.
Apply SepI to the current goal.
We will prove 0 ∈ SNoL x.
Apply SNoL_I x Hx 0 SNo_0 to the current goal.
We will prove SNoLev 0 ∈ SNoLev x.
rewrite the current goal using SNoLev_0 (from left to right).
An exact proof term for the current goal is H1.
We will prove 0 < x.
Apply SNoLeE 0 x SNo_0 Hx Hxnn to the current goal.
Assume H3: 0 < x.
An exact proof term for the current goal is H3.
Assume H3: 0 = x.
We will prove False.
Apply EmptyE 0 to the current goal.
rewrite the current goal using SNoLev_0 (from right to left) at position 2.
rewrite the current goal using H3 (from left to right) at position 2.
An exact proof term for the current goal is H1.
We will prove 0 ≤ 0.
Apply SNoLe_ref to the current goal.
∎