Let w be given.

Assume Hw: SNo w.

Let g and h be given.

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

We will prove H w g = H w h.

We will prove (λz : set ⇒ if SNo z then SNo_rec_i (G w g) z else Empty) = (λz : set ⇒ if SNo z then SNo_rec_i (G w h) z else Empty).

Apply func_ext set set to the current goal.

Let z be given.

We will prove (if SNo z then SNo_rec_i (G w g) z else Empty) = (if SNo z then SNo_rec_i (G w h) z else Empty).

Apply xm (SNo z) to the current goal.

Assume Hz: SNo z.

rewrite the current goal using If_i_1 (SNo z) (SNo_rec_i (G w g) z) Empty Hz (from left to right).

rewrite the current goal using If_i_1 (SNo z) (SNo_rec_i (G w h) z) Empty Hz (from left to right).

We will prove SNo_rec_i (G w g) z = SNo_rec_i (G w h) z.

We prove the intermediate claim L1a: ∀alpha, ordinal alpha → ∀z ∈ SNoS_ alpha, SNo_rec_i (G w g) z = SNo_rec_i (G w h) z.

Apply ordinal_ind to the current goal.

Let alpha be given.

Assume Ha: ordinal alpha.

Assume IH: ∀beta ∈ alpha, ∀z ∈ SNoS_ beta, SNo_rec_i (G w g) z = SNo_rec_i (G w h) z.

Let z be given.

Assume Hz: z ∈ SNoS_ alpha.

Apply SNoS_E2 alpha Ha z Hz to the current goal.

Assume Hz1: SNoLev z ∈ alpha.

Assume Hz2: ordinal (SNoLev z).

Assume Hz3: SNo z.

Assume Hz4: SNo_ (SNoLev z) z.

We will prove SNo_rec_i (G w g) z = SNo_rec_i (G w h) z.

rewrite the current goal using SNo_rec2_eq_1 w Hw g z Hz3 (from left to right).

rewrite the current goal using SNo_rec2_eq_1 w Hw h z Hz3 (from left to right).

We will prove G w g z (SNo_rec_i (G w g)) = G w h z (SNo_rec_i (G w h)).

Apply SNo_rec2_G_prop w Hw g h Hgh z Hz3 (SNo_rec_i (G w g)) (SNo_rec_i (G w h)) to the current goal.

We will prove ∀y ∈ SNoS_ (SNoLev z), SNo_rec_i (G w g) y = SNo_rec_i (G w h) y.

Let y be given.

Assume Hy: y ∈ SNoS_ (SNoLev z).

An exact proof term for the current goal is IH (SNoLev z) Hz1 y Hy.

An exact proof term for the current goal is L1a (ordsucc (SNoLev z)) (ordinal_ordsucc (SNoLev z) (SNoLev_ordinal z Hz)) z (SNoS_SNoLev z Hz).

Assume Hz: ¬ SNo z.

rewrite the current goal using If_i_0 (SNo z) (SNo_rec_i (G w h) z) Empty Hz (from left to right).

An exact proof term for the current goal is If_i_0 (SNo z) (SNo_rec_i (G w g) z) Empty Hz.

We will prove (if SNo z then SNo_rec_i (G w (SNo_rec_ii H)) z else Empty) = F w z SNo_rec2.

rewrite the current goal using If_i_1 (SNo z) (SNo_rec_i (G w (SNo_rec_ii H)) z) Empty Hz (from left to right).

We will prove SNo_rec_i (G w (SNo_rec_ii H)) z = F w z SNo_rec2.

We will prove SNo_rec_i (G w (SNo_rec_ii H)) z = F w z (SNo_rec_ii H).

rewrite the current goal using SNo_rec2_eq_1 w Hw (SNo_rec_ii H) z Hz (from left to right).

We will prove G w (SNo_rec_ii H) z (SNo_rec_i (G w (SNo_rec_ii H))) = F w z (SNo_rec_ii H).

We will prove F w z (λx y ⇒ if x = w then SNo_rec_i (G w (SNo_rec_ii H)) y else SNo_rec_ii H x y) = F w z (SNo_rec_ii H).

We prove the intermediate claim L2a: ∀x ∈ SNoS_ (SNoLev w), ∀y, SNo y → (if x = w then SNo_rec_i (G w (SNo_rec_ii H)) y else SNo_rec_ii H x y) = SNo_rec_ii H x y.

Let x be given.

Assume Hx: x ∈ SNoS_ (SNoLev w).

Let y be given.

Assume Hy: SNo 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.

An exact proof term for the current goal is If_i_0 (x = w) (SNo_rec_i (G w (SNo_rec_ii H)) y) (SNo_rec_ii H x y) Lxw.

We prove the intermediate claim L2b: ∀y ∈ SNoS_ (SNoLev z), (if w = w then SNo_rec_i (G w (SNo_rec_ii H)) y else SNo_rec_ii H w y) = SNo_rec_ii H w y.

Let y be given.

Assume Hy: y ∈ SNoS_ (SNoLev z).

rewrite the current goal using If_i_1 (w = w) (SNo_rec_i (G w (SNo_rec_ii H)) y) (SNo_rec_ii H w y) (λq H ⇒ H) (from left to right).

We prove the intermediate claim Ly: SNo y.

Apply SNoS_E2 (SNoLev z) (SNoLev_ordinal z Hz) y Hy to the current goal.

Assume Hy1: SNoLev y ∈ SNoLev z.

Assume Hy2: ordinal (SNoLev y).

Assume Hy3: SNo y.

Assume Hy4: SNo_ (SNoLev y) y.

An exact proof term for the current goal is Hy3.

We will prove SNo_rec_i (G w (SNo_rec_ii H)) y = SNo_rec_ii H w y.

Apply eq_i_tra (SNo_rec_i (G w (SNo_rec_ii H)) y) (H w (SNo_rec_ii H) y) (SNo_rec_ii H w y) to the current goal.

We will prove SNo_rec_i (G w (SNo_rec_ii H)) y = H w (SNo_rec_ii H) y.

We will prove SNo_rec_i (G w (SNo_rec_ii H)) y = if SNo y then (SNo_rec_i (G w (SNo_rec_ii H)) y) else Empty.

Use symmetry.

An exact proof term for the current goal is If_i_1 (SNo y) (SNo_rec_i (G w (SNo_rec_ii H)) y) Empty Ly.

We will prove H w (SNo_rec_ii H) y = SNo_rec_ii H w y.

rewrite the current goal using SNo_rec_ii_eq H L1 w Hw (from left to right).

We will prove H w (SNo_rec_ii H) y = H w (SNo_rec_ii H) y.

An exact proof term for the current goal is (λq H ⇒ H).

An exact proof term for the current goal is Fr w Hw z Hz (λx y ⇒ if x = w then SNo_rec_i (G w (SNo_rec_ii H)) y else SNo_rec_ii H x y) (SNo_rec_ii H) L2a L2b.