Let alpha, g and h be given.

Assume Hgh: ∀x ∈ alpha, g x = h x.

We will prove G alpha g = G alpha h.

We will prove (If_iii (ordinal alpha) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : set ⇒ default)) = (If_iii (ordinal alpha) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ h (SNoLev w) w)) default) (λz : set ⇒ default)).

Apply xm (ordinal alpha) to the current goal.

Assume H1: ordinal alpha.

rewrite the current goal using If_iii_1 (ordinal alpha) (λz ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ h (SNoLev w) w)) default) (λz : set ⇒ default) H1 (from left to right).

rewrite the current goal using If_iii_1 (ordinal alpha) (λz ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : set ⇒ default) H1 (from left to right).

We will prove (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default) = (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ h (SNoLev w) w)) default).

Apply func_ext set (set → set) to the current goal.

Let z be given.

We will prove (If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default) = (If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ h (SNoLev w) w)) default).

Apply xm (z ∈ SNoS_ (ordsucc alpha)) to the current goal.

Assume Hz: z ∈ SNoS_ (ordsucc alpha).

rewrite the current goal using If_ii_1 (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default Hz (from left to right).

rewrite the current goal using If_ii_1 (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ h (SNoLev w) w)) default Hz (from left to right).

We will prove F z (λw ⇒ g (SNoLev w) w) = F z (λw ⇒ h (SNoLev w) w).

We prove the intermediate claim Lsa: ordinal (ordsucc alpha).

An exact proof term for the current goal is ordinal_ordsucc alpha H1.

Apply SNoS_E2 (ordsucc alpha) Lsa z Hz to the current goal.

Assume Hz1: SNoLev z ∈ ordsucc alpha.

Assume Hz2: ordinal (SNoLev z).

Assume Hz3: SNo z.

Assume Hz4: SNo_ (SNoLev z) z.

We will prove F z (λw ⇒ g (SNoLev w) w) = F z (λw ⇒ h (SNoLev w) w).

Apply Fr to the current goal.

We will prove SNo z.

An exact proof term for the current goal is Hz3.

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

Let w be given.

Assume Hw: w ∈ SNoS_ (SNoLev z).

Apply SNoS_E2 (SNoLev z) Hz2 w Hw to the current goal.

Assume Hw1: SNoLev w ∈ SNoLev z.

Assume Hw2: ordinal (SNoLev w).

Assume Hw3: SNo w.

Assume Hw4: SNo_ (SNoLev w) w.

We prove the intermediate claim LLw: SNoLev w ∈ alpha.

Apply ordsuccE alpha (SNoLev z) Hz1 to the current goal.

Assume H2: SNoLev z ∈ alpha.

Apply H1 to the current goal.

Assume Ha1 _.

An exact proof term for the current goal is Ha1 (SNoLev z) H2 (SNoLev w) Hw1.

Assume H2: SNoLev z = alpha.

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

An exact proof term for the current goal is Hw1.

rewrite the current goal using Hgh (SNoLev w) LLw (from left to right).

Use reflexivity.

Assume Hz: z ∉ SNoS_ (ordsucc alpha).

rewrite the current goal using If_ii_0 (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ h (SNoLev w) w)) default Hz (from left to right).

An exact proof term for the current goal is If_ii_0 (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default Hz.

Assume H1: ¬ ordinal alpha.

rewrite the current goal using If_iii_0 (ordinal alpha) (λz ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ h (SNoLev w) w)) default) (λz : set ⇒ default) H1 (from left to right).

An exact proof term for the current goal is If_iii_0 (ordinal alpha) (λz ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : set ⇒ default) H1.