Set F to be the term λx y a ⇒ SNoCut ({a w y|w ∈ SNoL x} ∪ {a x w|w ∈ SNoL y}) ({a z y|z ∈ SNoR x} ∪ {a x z|z ∈ SNoR y}) of type set → set → (set → set → set) → set.
We prove the intermediate claim L1: ∀x, SNo x → ∀y, SNo y → ∀g h : set → set → set, (∀w ∈ SNoS_ (SNoLev x), ∀z, SNo z → g w z = h w z) → (∀z ∈ SNoS_ (SNoLev y), g x z = h x z) → F x y g = F x y h.
Let x be given.
Assume Hx: SNo x.
Let y be given.
Assume Hy: SNo y.
Let g and h be given.
Assume Hgh1: ∀w ∈ SNoS_ (SNoLev x), ∀z, SNo z → g w z = h w z.
Assume Hgh2: ∀z ∈ SNoS_ (SNoLev y), g x z = h x z.
We will prove F x y g = F x y h.
We prove the intermediate claim L1a: {g w y|w ∈ SNoL x} = {h w y|w ∈ SNoL x}.
Apply ReplEq_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
We will prove g w y = h w y.
Apply Hgh1 to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoL_SNoS x Hx w Hw.
We will prove SNo y.
An exact proof term for the current goal is Hy.
We prove the intermediate claim L1b: {g x w|w ∈ SNoL y} = {h x w|w ∈ SNoL y}.
Apply ReplEq_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL y.
We will prove g x w = h x w.
Apply Hgh2 to the current goal.
We will prove w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoL_SNoS y Hy w Hw.
We prove the intermediate claim L1c: {g z y|z ∈ SNoR x} = {h z y|z ∈ SNoR x}.
Apply ReplEq_ext to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR x.
We will prove g z y = h z y.
Apply Hgh1 to the current goal.
We will prove z ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoR_SNoS x Hx z Hz.
We will prove SNo y.
An exact proof term for the current goal is Hy.
We prove the intermediate claim L1d: {g x z|z ∈ SNoR y} = {h x z|z ∈ SNoR y}.
Apply ReplEq_ext to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR y.
We will prove g x z = h x z.
Apply Hgh2 to the current goal.
We will prove z ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoR_SNoS y Hy z Hz.
We will prove SNoCut ({g w y|w ∈ SNoL x} ∪ {g x w|w ∈ SNoL y}) ({g z y|z ∈ SNoR x} ∪ {g x z|z ∈ SNoR y}) = SNoCut ({h w y|w ∈ SNoL x} ∪ {h x w|w ∈ SNoL y}) ({h z y|z ∈ SNoR x} ∪ {h x z|z ∈ SNoR y}).
rewrite the current goal using L1a (from left to right).
rewrite the current goal using L1b (from left to right).
rewrite the current goal using L1c (from left to right).
rewrite the current goal using L1d (from left to right).
Use reflexivity.
An exact proof term for the current goal is SNo_rec2_eq F L1.
∎