Set L to be the term
⋃k ∈ ωL_ k.
Set R to be the term
⋃k ∈ ωR_ k.
We prove the intermediate
claim L1:
∀k, nat_p k → L_ k = 0 ∧ R_ k = 0.
Apply andI to the current goal.
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using
SNoL_nonneg_0 (from left to right).
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
rewrite the current goal using
SNoR_0 (from left to right).
Let k be given.
Assume Hk.
Assume IHk.
Apply IHk to the current goal.
Apply andI to the current goal.
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using IHLk (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
rewrite the current goal using IHLk (from left to right).
rewrite the current goal using IHRk (from left to right).
rewrite the current goal using
binunion_idl 0 (from left to right).
We prove the intermediate
claim L2:
L = 0.
Let x be given.
Let k be given.
Assume _.
rewrite the current goal using H1 (from left to right).
An
exact proof term for the current goal is
EmptyE x.
We prove the intermediate
claim L3:
R = 0.
Let x be given.
Let k be given.
Assume _.
rewrite the current goal using H1 (from left to right).
An
exact proof term for the current goal is
EmptyE x.
rewrite the current goal using L2 (from left to right).
rewrite the current goal using L3 (from left to right).
An
exact proof term for the current goal is
SNoCut_0_0.
∎