Let w be given.
Assume Hw: SNo w.
Let f and k be given.
Assume Hfk: ∀x ∈ SNoS_ (SNoLev w), f x = k x.
Let z be given.
Assume Hz: SNo z.
Let g and h be given.
Assume Hgh: ∀u ∈ SNoS_ (SNoLev z), g u = h u.
We will prove G w f z g = G w k z h.
We will prove F w z (λx y ⇒ if x = w then g y else f x y) = F w z (λx y ⇒ if x = w then h y else k x y).
Apply Fr to the current goal.
We will prove SNo w.
An exact proof term for the current goal is Hw.
We will prove SNo z.
An exact proof term for the current goal is Hz.
Let x be given.
Assume Hx: x ∈ SNoS_ (SNoLev w).
Let y be given.
Assume Hy: SNo y.
We will prove (if x = w then g y else f x y) = (if x = w then h y else k x y).
We prove the intermediate claim Lxw: x ≠ w.
An exact proof term for the current goal is SNoS_In_neq w Hw x Hx.
rewrite the current goal using If_i_0 (x = w) (g y) (f x y) Lxw (from left to right).
rewrite the current goal using If_i_0 (x = w) (h y) (k x y) Lxw (from left to right).
We will prove f x y = k x y.
rewrite the current goal using Hfk x Hx (from left to right).
Use reflexivity.
Let y be given.
Assume Hy: y ∈ SNoS_ (SNoLev z).
We will prove (if w = w then g y else f w y) = (if w = w then h y else k w y).
rewrite the current goal using If_i_1 (w = w) (g y) (f w y) (λq H ⇒ H) (from left to right).
rewrite the current goal using If_i_1 (w = w) (h y) (k w y) (λq H ⇒ H) (from left to right).
We will prove g y = h y.
An exact proof term for the current goal is Hgh y Hy.
∎