Let z be given.
Assume Hz: SNo z.
We will prove SNo_rec_ii z = F z SNo_rec_ii.
We will prove In_rec_iii G (SNoLev z) z = F z (λz ⇒ In_rec_iii G (SNoLev z) z).
We prove the intermediate claim L1: ∀α, ∀g h : set → set → (set → set), (∀x ∈ α, g x = h x) → G α g = G α h.
Let α, g and h be given.
Assume Hgh: ∀x ∈ α, g x = h x.
We will prove G α g = G α h.
We will prove (If_iii (ordinal α) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc α)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : set ⇒ default)) = (If_iii (ordinal α) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc α)) (F z (λw ⇒ h (SNoLev w) w)) default) (λz : set ⇒ default)).
Apply xm (ordinal α) to the current goal.
Assume H1: ordinal α.
rewrite the current goal using If_iii_1 (ordinal α) (λz ⇒ If_ii (z ∈ SNoS_ (ordsucc α)) (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 α) (λz ⇒ If_ii (z ∈ SNoS_ (ordsucc α)) (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 α)) (F z (λw ⇒ g (SNoLev w) w)) default) = (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc α)) (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 α)) (F z (λw ⇒ g (SNoLev w) w)) default) = (If_ii (z ∈ SNoS_ (ordsucc α)) (F z (λw ⇒ h (SNoLev w) w)) default).
Apply xm (z ∈ SNoS_ (ordsucc α)) to the current goal.
Assume Hz: z ∈ SNoS_ (ordsucc α).
rewrite the current goal using If_ii_1 (z ∈ SNoS_ (ordsucc α)) (F z (λw ⇒ g (SNoLev w) w)) default Hz (from left to right).
rewrite the current goal using If_ii_1 (z ∈ SNoS_ (ordsucc α)) (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 α).
An exact proof term for the current goal is ordinal_ordsucc α H1.
Apply SNoS_E2 (ordsucc α) Lsa z Hz to the current goal.
Assume Hz1: SNoLev z ∈ ordsucc α.
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 ∈ α.
Apply ordsuccE α (SNoLev z) Hz1 to the current goal.
Assume H2: SNoLev z ∈ α.
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 = α.
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 α).
rewrite the current goal using If_ii_0 (z ∈ SNoS_ (ordsucc α)) (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 α)) (F z (λw ⇒ g (SNoLev w) w)) default Hz.
Assume H1: ¬ ordinal α.
rewrite the current goal using If_iii_0 (ordinal α) (λz ⇒ If_ii (z ∈ SNoS_ (ordsucc α)) (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 α) (λz ⇒ If_ii (z ∈ SNoS_ (ordsucc α)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : set ⇒ default) H1.
rewrite the current goal using In_rec_iii_eq G L1 (from left to right).
We will prove G (SNoLev z) (In_rec_iii G) z = F z (λz ⇒ In_rec_iii G (SNoLev z) z).
We will prove (If_iii (ordinal (SNoLev z)) (λu : set ⇒ If_ii (u ∈ SNoS_ (ordsucc (SNoLev z))) (F u (λw : set ⇒ In_rec_iii G (SNoLev w) w)) default) (λ_ : set ⇒ default)) z = F z (λz ⇒ In_rec_iii 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_iii_1 (ordinal (SNoLev z)) (λu : set ⇒ If_ii (u ∈ SNoS_ (ordsucc (SNoLev z))) (F u (λw : set ⇒ In_rec_iii G (SNoLev w) w)) default) (λ_ : set ⇒ default) L2 (from left to right).
We will prove (If_ii (z ∈ SNoS_ (ordsucc (SNoLev z))) (F z (λw : set ⇒ In_rec_iii G (SNoLev w) w)) default) = F z (λz ⇒ In_rec_iii 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_ii_1 (z ∈ SNoS_ (ordsucc (SNoLev z))) (F z (λw : set ⇒ In_rec_iii G (SNoLev w) w)) default L3.
∎