Let z be given.
Assume Hz: SNo z.
We will prove SNo_rec_i z = F z SNo_rec_i.
We will prove In_rec_ii G (SNoLev z) z = F z (λz ⇒ In_rec_ii G (SNoLev z) z).
We prove the intermediate claim L1: ∀alpha, ∀g h : set → set → set, (∀x ∈ alpha, g x = h x) → G alpha g = G alpha h.
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_ii (ordinal alpha) (λz : set ⇒ if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ g (SNoLev w) w) else default) (λz : set ⇒ default)) = (If_ii (ordinal alpha) (λz : set ⇒ if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ h (SNoLev w) w) else default) (λz : set ⇒ default)).
Apply xm (ordinal alpha) to the current goal.
Assume H1: ordinal alpha.
rewrite the current goal using If_ii_1 (ordinal alpha) (λz ⇒ if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ h (SNoLev w) w) else default) (λz : set ⇒ default) H1 (from left to right).
rewrite the current goal using If_ii_1 (ordinal alpha) (λz ⇒ if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ g (SNoLev w) w) else default) (λz : set ⇒ default) H1 (from left to right).
We will prove (λz : set ⇒ if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ g (SNoLev w) w) else default) = (λz : set ⇒ if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ h (SNoLev w) w) else default).
Apply func_ext set set to the current goal.
Let z be given.
We will prove (if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ g (SNoLev w) w) else default) = (if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ h (SNoLev w) w) else default).
Apply xm (z ∈ SNoS_ (ordsucc alpha)) to the current goal.
Assume Hz: z ∈ SNoS_ (ordsucc alpha).
rewrite the current goal using If_i_1 (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default Hz (from left to right).
rewrite the current goal using If_i_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_i_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_i_0 (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default Hz.
Assume H1: ¬ ordinal alpha.
rewrite the current goal using If_ii_0 (ordinal alpha) (λz ⇒ if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ h (SNoLev w) w) else default) (λz : set ⇒ default) H1 (from left to right).
An exact proof term for the current goal is If_ii_0 (ordinal alpha) (λz ⇒ if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ g (SNoLev w) w) else default) (λz : set ⇒ default) H1.
rewrite the current goal using In_rec_ii_eq G L1 (from left to right).
We will prove G (SNoLev z) (In_rec_ii G) z = F z (λz ⇒ In_rec_ii G (SNoLev z) z).
We will prove (If_ii (ordinal (SNoLev z)) (λu : set ⇒ if u ∈ SNoS_ (ordsucc (SNoLev z)) then F u (λw : set ⇒ In_rec_ii G (SNoLev w) w) else default) (λ_ : set ⇒ default)) z = F z (λz ⇒ In_rec_ii G (SNoLev z) z).
We prove the intermediate claim L2: ordinal (SNoLev z).
An exact proof term for the current goal is SNoLev_ordinal z Hz.
rewrite the current goal using If_ii_1 (ordinal (SNoLev z)) (λu : set ⇒ if u ∈ SNoS_ (ordsucc (SNoLev z)) then F u (λw : set ⇒ In_rec_ii G (SNoLev w) w) else default) (λ_ : set ⇒ default) L2 (from left to right).
We will prove (if z ∈ SNoS_ (ordsucc (SNoLev z)) then F z (λw : set ⇒ In_rec_ii G (SNoLev w) w) else default) = F z (λz ⇒ In_rec_ii G (SNoLev z) z).
We prove the intermediate claim L3: z ∈ SNoS_ (ordsucc (SNoLev z)).
An exact proof term for the current goal is SNoS_SNoLev z Hz.
An exact proof term for the current goal is If_i_1 (z ∈ SNoS_ (ordsucc (SNoLev z))) (F z (λw : set ⇒ In_rec_ii G (SNoLev w) w)) default L3.
∎