We prove the intermediate claim L1: ∀x, SNo x → ∀g h : set → set, (∀w ∈ SNoS_ (SNoLev x), g w = h w) → SNoCut {g z|z ∈ SNoR x} {g w|w ∈ SNoL x} = SNoCut {h z|z ∈ SNoR x} {h w|w ∈ SNoL x}.

Let x be given.

Assume Hx: SNo x.

Let g and h be given.

Assume Hgh: ∀w ∈ SNoS_ (SNoLev x), g w = h w.

We will prove SNoCut {g z|z ∈ SNoR x} {g w|w ∈ SNoL x} = SNoCut {h z|z ∈ SNoR x} {h w|w ∈ SNoL x}.

We prove the intermediate claim L1a: {g z|z ∈ SNoR x} = {h z|z ∈ SNoR x}.

Apply ReplEq_ext to the current goal.

Let z be given.

Assume Hz: z ∈ SNoR x.

We will prove g z = h z.

Apply Hgh 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 prove the intermediate claim L1b: {g w|w ∈ SNoL x} = {h w|w ∈ SNoL x}.

Apply ReplEq_ext to the current goal.

Let w be given.

Assume Hw: w ∈ SNoL x.

We will prove g w = h w.

Apply Hgh 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.

rewrite the current goal using L1a (from left to right).

rewrite the current goal using L1b (from left to right).

Use reflexivity.