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 0) y + g x (w 1) + - g (w 0) (w 1)|w ∈ SNoL x ⨯ SNoL y} = {h (w 0) y + h x (w 1) + - h (w 0) (w 1)|w ∈ SNoL x ⨯ SNoL y}.

Apply ReplEq_setprod_ext (SNoL x) (SNoL y) (λw0 w1 ⇒ g w0 y + g x w1 + - g w0 w1) (λw0 w1 ⇒ h w0 y + h x w1 + - h w0 w1) to the current goal.

We will prove ∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, g w0 y + g x w1 + - g w0 w1 = h w0 y + h x w1 + - h w0 w1.

Let w0 be given.

Assume Hw0: w0 ∈ SNoL x.

Let w1 be given.

Assume Hw1: w1 ∈ SNoL y.

We prove the intermediate claim Lw0: w0 ∈ SNoS_ (SNoLev x).

An exact proof term for the current goal is SNoL_SNoS x Hx w0 Hw0.

We prove the intermediate claim Lw1: w1 ∈ SNoS_ (SNoLev y).

An exact proof term for the current goal is SNoL_SNoS y Hy w1 Hw1.

We prove the intermediate claim Lw1b: SNo w1.

Apply SNoL_E y Hy w1 Hw1 to the current goal.

Assume H _ _.

An exact proof term for the current goal is H.

We prove the intermediate claim L1aa: g w0 y = h w0 y.

Apply Hgh1 to the current goal.

An exact proof term for the current goal is Lw0.

An exact proof term for the current goal is Hy.

We prove the intermediate claim L1ab: g x w1 = h x w1.

Apply Hgh2 to the current goal.

An exact proof term for the current goal is Lw1.

We prove the intermediate claim L1ac: g w0 w1 = h w0 w1.

Apply Hgh1 to the current goal.

An exact proof term for the current goal is Lw0.

An exact proof term for the current goal is Lw1b.

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

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

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

Use reflexivity.

We prove the intermediate claim L1b: {g (z 0) y + g x (z 1) + - g (z 0) (z 1)|z ∈ SNoR x ⨯ SNoR y} = {h (z 0) y + h x (z 1) + - h (z 0) (z 1)|z ∈ SNoR x ⨯ SNoR y}.

Apply ReplEq_setprod_ext (SNoR x) (SNoR y) (λz0 z1 ⇒ g z0 y + g x z1 + - g z0 z1) (λz0 z1 ⇒ h z0 y + h x z1 + - h z0 z1) to the current goal.

We will prove ∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, g z0 y + g x z1 + - g z0 z1 = h z0 y + h x z1 + - h z0 z1.

Let z0 be given.

Assume Hz0: z0 ∈ SNoR x.

Let z1 be given.

Assume Hz1: z1 ∈ SNoR y.

We prove the intermediate claim Lz0: z0 ∈ SNoS_ (SNoLev x).

An exact proof term for the current goal is SNoR_SNoS x Hx z0 Hz0.

We prove the intermediate claim Lz1: z1 ∈ SNoS_ (SNoLev y).

An exact proof term for the current goal is SNoR_SNoS y Hy z1 Hz1.

We prove the intermediate claim Lz1b: SNo z1.

Apply SNoR_E y Hy z1 Hz1 to the current goal.

Assume H _ _.

An exact proof term for the current goal is H.

We prove the intermediate claim L1ba: g z0 y = h z0 y.

Apply Hgh1 to the current goal.

An exact proof term for the current goal is Lz0.

An exact proof term for the current goal is Hy.

We prove the intermediate claim L1bb: g x z1 = h x z1.

Apply Hgh2 to the current goal.

An exact proof term for the current goal is Lz1.

We prove the intermediate claim L1bc: g z0 z1 = h z0 z1.

Apply Hgh1 to the current goal.

An exact proof term for the current goal is Lz0.

An exact proof term for the current goal is Lz1b.

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

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

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

Use reflexivity.

We prove the intermediate claim L1c: {g (w 0) y + g x (w 1) + - g (w 0) (w 1)|w ∈ SNoL x ⨯ SNoR y} = {h (w 0) y + h x (w 1) + - h (w 0) (w 1)|w ∈ SNoL x ⨯ SNoR y}.

Apply ReplEq_setprod_ext (SNoL x) (SNoR y) (λw0 w1 ⇒ g w0 y + g x w1 + - g w0 w1) (λw0 w1 ⇒ h w0 y + h x w1 + - h w0 w1) to the current goal.

We will prove ∀w0 ∈ SNoL x, ∀w1 ∈ SNoR y, g w0 y + g x w1 + - g w0 w1 = h w0 y + h x w1 + - h w0 w1.

Let w0 be given.

Assume Hw0: w0 ∈ SNoL x.

Let w1 be given.

Assume Hw1: w1 ∈ SNoR y.

We prove the intermediate claim Lw0: w0 ∈ SNoS_ (SNoLev x).

An exact proof term for the current goal is SNoL_SNoS x Hx w0 Hw0.

We prove the intermediate claim Lw1: w1 ∈ SNoS_ (SNoLev y).

An exact proof term for the current goal is SNoR_SNoS y Hy w1 Hw1.

We prove the intermediate claim Lw1b: SNo w1.

Apply SNoR_E y Hy w1 Hw1 to the current goal.

Assume H _ _.

An exact proof term for the current goal is H.

We prove the intermediate claim L1ca: g w0 y = h w0 y.

Apply Hgh1 to the current goal.

An exact proof term for the current goal is Lw0.

An exact proof term for the current goal is Hy.

We prove the intermediate claim L1cb: g x w1 = h x w1.

Apply Hgh2 to the current goal.

An exact proof term for the current goal is Lw1.

We prove the intermediate claim L1cc: g w0 w1 = h w0 w1.

Apply Hgh1 to the current goal.

An exact proof term for the current goal is Lw0.

An exact proof term for the current goal is Lw1b.

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

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

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

Use reflexivity.

We prove the intermediate claim L1d: {g (z 0) y + g x (z 1) + - g (z 0) (z 1)|z ∈ SNoR x ⨯ SNoL y} = {h (z 0) y + h x (z 1) + - h (z 0) (z 1)|z ∈ SNoR x ⨯ SNoL y}.

Apply ReplEq_setprod_ext (SNoR x) (SNoL y) (λz0 z1 ⇒ g z0 y + g x z1 + - g z0 z1) (λz0 z1 ⇒ h z0 y + h x z1 + - h z0 z1) to the current goal.

We will prove ∀z0 ∈ SNoR x, ∀z1 ∈ SNoL y, g z0 y + g x z1 + - g z0 z1 = h z0 y + h x z1 + - h z0 z1.

Let z0 be given.

Assume Hz0: z0 ∈ SNoR x.

Let z1 be given.

Assume Hz1: z1 ∈ SNoL y.

We prove the intermediate claim Lz0: z0 ∈ SNoS_ (SNoLev x).

An exact proof term for the current goal is SNoR_SNoS x Hx z0 Hz0.

We prove the intermediate claim Lz1: z1 ∈ SNoS_ (SNoLev y).

An exact proof term for the current goal is SNoL_SNoS y Hy z1 Hz1.

We prove the intermediate claim Lz1b: SNo z1.

Apply SNoL_E y Hy z1 Hz1 to the current goal.

Assume H _ _.

An exact proof term for the current goal is H.

We prove the intermediate claim L1da: g z0 y = h z0 y.

Apply Hgh1 to the current goal.

An exact proof term for the current goal is Lz0.

An exact proof term for the current goal is Hy.

We prove the intermediate claim L1db: g x z1 = h x z1.

Apply Hgh2 to the current goal.

An exact proof term for the current goal is Lz1.

We prove the intermediate claim L1dc: g z0 z1 = h z0 z1.

Apply Hgh1 to the current goal.

An exact proof term for the current goal is Lz0.

An exact proof term for the current goal is Lz1b.

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

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

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

Use reflexivity.

We will prove SNoCut ({g (w 0) y + g x (w 1) + - g (w 0) (w 1)|w ∈ SNoL x ⨯ SNoL y} ∪ {g (z 0) y + g x (z 1) + - g (z 0) (z 1)|z ∈ SNoR x ⨯ SNoR y}) ({g (w 0) y + g x (w 1) + - g (w 0) (w 1)|w ∈ SNoL x ⨯ SNoR y} ∪ {g (z 0) y + g x (z 1) + - g (z 0) (z 1)|z ∈ SNoR x ⨯ SNoL y}) = SNoCut ({h (w 0) y + h x (w 1) + - h (w 0) (w 1)|w ∈ SNoL x ⨯ SNoL y} ∪ {h (z 0) y + h x (z 1) + - h (z 0) (z 1)|z ∈ SNoR x ⨯ SNoR y}) ({h (w 0) y + h x (w 1) + - h (w 0) (w 1)|w ∈ SNoL x ⨯ SNoR y} ∪ {h (z 0) y + h x (z 1) + - h (z 0) (z 1)|z ∈ SNoR x ⨯ SNoL 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.