Let x be given.
Assume Hx Hxnn H1.
Set L_ to be the term λk : set ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 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.
Apply SNoLeE 0 x SNo_0 Hx Hxnn to the current goal.
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.
Apply SNoLe_ref to the current goal.
∎