Let x be given.
Assume Hx.
Let g and h be given.
Assume Hgh.
Apply nat_ind to the current goal.
We will prove SNo_recipaux x g 0 = SNo_recipaux x h 0.
rewrite the current goal using SNo_recipaux_0 x h (from left to right).
An exact proof term for the current goal is SNo_recipaux_0 x g.
Let k be given.
Assume Hk: nat_p k.
Assume IH: SNo_recipaux x g k = SNo_recipaux x h k.
We will prove SNo_recipaux x g (ordsucc k) = SNo_recipaux x h (ordsucc k).
rewrite the current goal using SNo_recipaux_S x g k Hk (from left to right).
rewrite the current goal using SNo_recipaux_S x h k Hk (from left to right).
We will prove (SNo_recipaux x g k 0 ∪ SNo_recipauxset (SNo_recipaux x g k 0) x (SNoR x) g ∪ SNo_recipauxset (SNo_recipaux x g k 1) x (SNoL_pos x) g,SNo_recipaux x g k 1 ∪ SNo_recipauxset (SNo_recipaux x g k 0) x (SNoL_pos x) g ∪ SNo_recipauxset (SNo_recipaux x g k 1) x (SNoR x) g) = (SNo_recipaux x h k 0 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) h ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) h,SNo_recipaux x h k 1 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) h ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) h).
rewrite the current goal using IH (from left to right).
We will prove (SNo_recipaux x h k 0 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) g ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) g,SNo_recipaux x h k 1 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) g ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) g) = (SNo_recipaux x h k 0 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) h ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) h,SNo_recipaux x h k 1 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) h ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) h).
We prove the intermediate claim L1: SNo_recipaux x h k 0 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) g ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) g = SNo_recipaux x h k 0 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) h ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) h.
Use f_equal.
Use f_equal.
We will prove SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) g = SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) h.
Apply SNo_recipauxset_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
We will prove g w = h w.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
We will prove SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) g = SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) h.
Apply SNo_recipauxset_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL_pos x.
We will prove g w = h w.
Apply SNoL_E x Hx w (SepE1 (SNoL x) (λw ⇒ 0 < w) w Hw) to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
We prove the intermediate claim L2: SNo_recipaux x h k 1 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) g ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) g = SNo_recipaux x h k 1 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) h ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) h.
Use f_equal.
Use f_equal.
We will prove SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) g = SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) h.
Apply SNo_recipauxset_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL_pos x.
We will prove g w = h w.
Apply SNoL_E x Hx w (SepE1 (SNoL x) (λw ⇒ 0 < w) w Hw) to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
We will prove SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) g = SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) h.
Apply SNo_recipauxset_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
We will prove g w = h w.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
rewrite the current goal using L1 (from left to right).
rewrite the current goal using L2 (from left to right).
Use reflexivity.
∎