Apply nat_ind to the current goal.
We will prove equip {x ∈ SNoS_ ω|SNoLev x = 0} (2 ^ 0).
rewrite the current goal using exp_SNo_nat_0 2 SNo_2 (from left to right).
We will prove equip {x ∈ SNoS_ ω|SNoLev x = 0} 1.
Apply equip_sym to the current goal.
We will prove ∃f : set → set, bij 1 {x ∈ SNoS_ ω|SNoLev x = 0} f.
Set f to be the term λi : set ⇒ 0.
We use f to witness the existential quantifier.
Apply bijI to the current goal.
Let i be given.
Assume Hi: i ∈ 1.
We will prove 0 ∈ {x ∈ SNoS_ ω|SNoLev x = 0}.
Apply SepI to the current goal.
We will prove 0 ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal 0 0 (nat_p_omega 0 nat_0) to the current goal.
We will prove SNo_ 0 0.
An exact proof term for the current goal is ordinal_SNo_ 0 ordinal_Empty.
We will prove SNoLev 0 = 0.
An exact proof term for the current goal is SNoLev_0.
Let i be given.
Assume Hi: i ∈ 1.
Let j be given.
Assume Hj: j ∈ 1.
Assume Hij: 0 = 0.
We will prove i = j.
Apply cases_1 i Hi to the current goal.
Apply cases_1 j Hj to the current goal.
We will prove 0 = 0.
An exact proof term for the current goal is Hij.
Let x be given.
Assume Hx: x ∈ {x ∈ SNoS_ ω|SNoLev x = 0}.
Apply SepE (SNoS_ ω) (λx ⇒ SNoLev x = 0) x Hx to the current goal.
Assume Hx1: x ∈ SNoS_ ω.
Assume Hx2: SNoLev x = 0.
Apply SNoS_E2 ω omega_ordinal x Hx1 to the current goal.
Assume Hx1a: SNoLev x ∈ ω.
Assume Hx1b: ordinal (SNoLev x).
Assume Hx1c: SNo x.
Assume Hx1d: SNo_ (SNoLev x) x.
We prove the intermediate claim L1: x = 0.
Use symmetry.
Apply SNo_eq 0 x SNo_0 Hx1c to the current goal.
We will prove SNoLev 0 = SNoLev x.
rewrite the current goal using SNoLev_0 (from left to right).
Use symmetry.
An exact proof term for the current goal is Hx2.
We will prove SNoEq_ (SNoLev 0) 0 x.
rewrite the current goal using SNoLev_0 (from left to right).
Let α be given.
Assume Ha: α ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE α Ha.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is In_0_1.
We will prove 0 = x.
Use symmetry.
An exact proof term for the current goal is L1.
Let n be given.
Assume Hn.
Assume IHn: equip {x ∈ SNoS_ ω|SNoLev x = n} (2 ^ n).
We will prove equip {x ∈ SNoS_ ω|SNoLev x = ordsucc n} (2 ^ ordsucc n).
rewrite the current goal using exp_SNo_nat_S 2 SNo_2 n Hn (from left to right).
We will prove equip {x ∈ SNoS_ ω|SNoLev x = ordsucc n} (2 * 2 ^ n).
rewrite the current goal using add_SNo_1_1_2 (from right to left) at position 1.
We will prove equip {x ∈ SNoS_ ω|SNoLev x = ordsucc n} ((1 + 1) * 2 ^ n).
rewrite the current goal using mul_SNo_distrR 1 1 (2 ^ n) SNo_1 SNo_1 (SNo_exp_SNo_nat 2 SNo_2 n Hn) (from left to right).
rewrite the current goal using mul_SNo_oneL (2 ^ n) (SNo_exp_SNo_nat 2 SNo_2 n Hn) (from left to right).
We will prove equip {x ∈ SNoS_ ω|SNoLev x = ordsucc n} (2 ^ n + 2 ^ n).
We prove the intermediate claim L2n1: nat_p (2 ^ n).
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 n Hn.
We prove the intermediate claim L2n2: ordinal (2 ^ n).
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is L2n1.
We prove the intermediate claim L2n3: SNo (2 ^ n).
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is L2n2.
We prove the intermediate claim L2n2n1: nat_p (2 ^ n + 2 ^ n).
Apply omega_nat_p to the current goal.
Apply add_SNo_In_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is L2n1.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is L2n1.
We prove the intermediate claim L2n2n2: ordinal (2 ^ n + 2 ^ n).
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is L2n2n1.
We prove the intermediate claim L2n2n3: SNo (2 ^ n + 2 ^ n).
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is L2n2n2.
We prove the intermediate claim L2npLt2n2n: ∀m, SNo m → m < 2 ^ n → 2 ^ n + m < 2 ^ n + 2 ^ n.
Let m be given.
Assume Hm H1.
An exact proof term for the current goal is add_SNo_Lt2 (2 ^ n) m (2 ^ n) L2n3 Hm L2n3 H1.
We prove the intermediate claim L2nLt2n2n: 2 ^ n < 2 ^ n + 2 ^ n.
rewrite the current goal using add_SNo_0R (2 ^ n) L2n3 (from right to left) at position 1.
We will prove 2 ^ n + 0 < 2 ^ n + 2 ^ n.
Apply L2npLt2n2n 0 SNo_0 to the current goal.
We will prove 0 < 2 ^ n.
An exact proof term for the current goal is exp_SNo_nat_pos 2 SNo_2 SNoLt_0_2 n Hn.
Apply IHn to the current goal.
Let f be given.
Assume Hf: bij {x ∈ SNoS_ ω|SNoLev x = n} (2 ^ n) f.
Apply bijE {x ∈ SNoS_ ω|SNoLev x = n} (2 ^ n) f Hf to the current goal.
Assume Hf1: ∀u ∈ {x ∈ SNoS_ ω|SNoLev x = n}, f u ∈ (2 ^ n).
Assume Hf2: ∀u v ∈ {x ∈ SNoS_ ω|SNoLev x = n}, f u = f v → u = v.
Assume Hf3: ∀w ∈ 2 ^ n, ∃u ∈ {x ∈ SNoS_ ω|SNoLev x = n}, f u = w.
We prove the intermediate claim L2: ∀x ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}, ∀p : prop, (SNo x → SNoLev x = ordsucc n → (x ∩ SNoElts_ n) ∈ {x ∈ SNoS_ ω|SNoLev x = n} → SNo (x ∩ SNoElts_ n) → SNoLev (x ∩ SNoElts_ n) = n → p) → p.
Let x be given.
Assume Hx.
Apply SepE (SNoS_ ω) (λx ⇒ SNoLev x = ordsucc n) x Hx to the current goal.
Assume Hx HxSn.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume Hx1: SNoLev x ∈ ω.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
Let p be given.
Assume Hp.
We prove the intermediate claim L2a: n ∈ SNoLev x.
rewrite the current goal using HxSn (from left to right).
Apply ordsuccI2 to the current goal.
We prove the intermediate claim L2b: SNoLev (x ∩ SNoElts_ n) = n.
An exact proof term for the current goal is restr_SNoLev x Hx3 n L2a.
Apply Hp to the current goal.
An exact proof term for the current goal is Hx3.
An exact proof term for the current goal is HxSn.
Apply SepI to the current goal.
We will prove (x ∩ SNoElts_ n) ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal (x ∩ SNoElts_ n) n (nat_p_omega n Hn) to the current goal.
We will prove SNo_ n (x ∩ SNoElts_ n).
An exact proof term for the current goal is restr_SNo_ x Hx3 n L2a.
We will prove SNoLev (x ∩ SNoElts_ n) = n.
An exact proof term for the current goal is L2b.
An exact proof term for the current goal is restr_SNo x Hx3 n L2a.
An exact proof term for the current goal is L2b.
We prove the intermediate claim Lf: ∀u ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}, ∀p : prop, (nat_p (f (u ∩ SNoElts_ n)) → ordinal (f (u ∩ SNoElts_ n)) → SNo (f (u ∩ SNoElts_ n)) → f (u ∩ SNoElts_ n) < 2 ^ n → p) → p.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply L2 u Hu to the current goal.
Assume Hu0a: SNo u.
Assume Hu0b: SNoLev u = ordsucc n.
Assume Hu1: (u ∩ SNoElts_ n) ∈ {x ∈ SNoS_ ω|SNoLev x = n}.
Assume Hu2: SNo (u ∩ SNoElts_ n).
Assume Hu3: SNoLev (u ∩ SNoElts_ n) = n.
We prove the intermediate claim Lf1a: f (u ∩ SNoElts_ n) ∈ 2 ^ n.
An exact proof term for the current goal is Hf1 (u ∩ SNoElts_ n) Hu1.
We prove the intermediate claim Lf1b: nat_p (f (u ∩ SNoElts_ n)).
An exact proof term for the current goal is nat_p_trans (2 ^ n) L2n1 (f (u ∩ SNoElts_ n)) Lf1a.
We prove the intermediate claim Lf1c: ordinal (f (u ∩ SNoElts_ n)).
An exact proof term for the current goal is nat_p_ordinal (f (u ∩ SNoElts_ n)) Lf1b.
Apply Hp to the current goal.
An exact proof term for the current goal is Lf1b.
An exact proof term for the current goal is Lf1c.
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is Lf1c.
Apply ordinal_In_SNoLt to the current goal.
We will prove ordinal (2 ^ n).
An exact proof term for the current goal is L2n2.
We will prove f (u ∩ SNoElts_ n) ∈ 2 ^ n.
An exact proof term for the current goal is Lf1a.
We prove the intermediate claim Lg: ∃g : set → set, (∀x, n ∈ x → g x = f (x ∩ SNoElts_ n)) ∧ (∀x, n ∉ x → g x = 2 ^ n + f (x ∩ SNoElts_ n)).
We use (λx ⇒ if n ∈ x then f (x ∩ SNoElts_ n) else 2 ^ n + f (x ∩ SNoElts_ n)) to witness the existential quantifier.
Apply andI to the current goal.
Let x be given.
Assume H1: n ∈ x.
An exact proof term for the current goal is If_i_1 (n ∈ x) (f (x ∩ SNoElts_ n)) (2 ^ n + f (x ∩ SNoElts_ n)) H1.
Let x be given.
Assume H1: n ∉ x.
An exact proof term for the current goal is If_i_0 (n ∈ x) (f (x ∩ SNoElts_ n)) (2 ^ n + f (x ∩ SNoElts_ n)) H1.
Apply Lg to the current goal.
Let g be given.
Assume H.
Apply H to the current goal.
Assume Hg1: ∀x, n ∈ x → g x = f (x ∩ SNoElts_ n).
Assume Hg2: ∀x, n ∉ x → g x = 2 ^ n + f (x ∩ SNoElts_ n).
We will prove ∃g : set → set, bij {x ∈ SNoS_ ω|SNoLev x = ordsucc n} (2 ^ n + 2 ^ n) g.
We use g to witness the existential quantifier.
Apply bijI to the current goal.
Let u be given.
Assume Hu: u ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}.
We will prove g u ∈ 2 ^ n + 2 ^ n.
Apply L2 u Hu to the current goal.
Assume Hu0a: SNo u.
Assume Hu0b: SNoLev u = ordsucc n.
Assume Hu1: (u ∩ SNoElts_ n) ∈ {x ∈ SNoS_ ω|SNoLev x = n}.
Assume Hu2: SNo (u ∩ SNoElts_ n).
Assume Hu3: SNoLev (u ∩ SNoElts_ n) = n.
Apply Lf u Hu to the current goal.
Assume Lfu1: nat_p (f (u ∩ SNoElts_ n)).
Assume Lfu2: ordinal (f (u ∩ SNoElts_ n)).
Assume Lfu3: SNo (f (u ∩ SNoElts_ n)).
Assume Lfu4: f (u ∩ SNoElts_ n) < 2 ^ n.
Apply xm (n ∈ u) to the current goal.
Assume H1: n ∈ u.
rewrite the current goal using Hg1 u H1 (from left to right).
We will prove f (u ∩ SNoElts_ n) ∈ 2 ^ n + 2 ^ n.
Apply ordinal_SNoLt_In (f (u ∩ SNoElts_ n)) (2 ^ n + 2 ^ n) Lfu2 L2n2n2 to the current goal.
We will prove f (u ∩ SNoElts_ n) < 2 ^ n + 2 ^ n.
An exact proof term for the current goal is SNoLt_tra (f (u ∩ SNoElts_ n)) (2 ^ n) (2 ^ n + 2 ^ n) Lfu3 L2n3 L2n2n3 Lfu4 L2nLt2n2n.
Assume H1: n ∉ u.
rewrite the current goal using Hg2 u H1 (from left to right).
We will prove 2 ^ n + f (u ∩ SNoElts_ n) ∈ 2 ^ n + 2 ^ n.
Apply ordinal_SNoLt_In (2 ^ n + f (u ∩ SNoElts_ n)) (2 ^ n + 2 ^ n) (add_SNo_ordinal_ordinal (2 ^ n) L2n2 (f (u ∩ SNoElts_ n)) Lfu2) L2n2n2 to the current goal.
We will prove 2 ^ n + f (u ∩ SNoElts_ n) < 2 ^ n + 2 ^ n.
An exact proof term for the current goal is L2npLt2n2n (f (u ∩ SNoElts_ n)) Lfu3 Lfu4.
Let u be given.
Assume Hu: u ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}.
Let v be given.
Assume Hv: v ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}.
Apply L2 u Hu to the current goal.
Assume Hu0a: SNo u.
Assume Hu0b: SNoLev u = ordsucc n.
Assume Hu1: (u ∩ SNoElts_ n) ∈ {x ∈ SNoS_ ω|SNoLev x = n}.
Assume Hu2: SNo (u ∩ SNoElts_ n).
Assume Hu3: SNoLev (u ∩ SNoElts_ n) = n.
Apply Lf u Hu to the current goal.
Assume Lfu1: nat_p (f (u ∩ SNoElts_ n)).
Assume Lfu2: ordinal (f (u ∩ SNoElts_ n)).
Assume Lfu3: SNo (f (u ∩ SNoElts_ n)).
Assume Lfu4: f (u ∩ SNoElts_ n) < 2 ^ n.
Apply L2 v Hv to the current goal.
Assume Hv0a: SNo v.
Assume Hv0b: SNoLev v = ordsucc n.
Assume Hv1: (v ∩ SNoElts_ n) ∈ {x ∈ SNoS_ ω|SNoLev x = n}.
Assume Hv2: SNo (v ∩ SNoElts_ n).
Assume Hv3: SNoLev (v ∩ SNoElts_ n) = n.
Apply Lf v Hv to the current goal.
Assume Lfv1: nat_p (f (v ∩ SNoElts_ n)).
Assume Lfv2: ordinal (f (v ∩ SNoElts_ n)).
Assume Lfv3: SNo (f (v ∩ SNoElts_ n)).
Assume Lfv4: f (v ∩ SNoElts_ n) < 2 ^ n.
We prove the intermediate claim LnLu: n ∈ SNoLev u.
rewrite the current goal using Hu0b (from left to right).
Apply ordsuccI2 to the current goal.
We prove the intermediate claim LnLv: n ∈ SNoLev v.
rewrite the current goal using Hv0b (from left to right).
Apply ordsuccI2 to the current goal.
Apply xm (n ∈ u) to the current goal.
Assume H1: n ∈ u.
rewrite the current goal using Hg1 u H1 (from left to right).
Apply xm (n ∈ v) to the current goal.
Assume H2: n ∈ v.
rewrite the current goal using Hg1 v H2 (from left to right).
Assume Hguv: f (u ∩ SNoElts_ n) = f (v ∩ SNoElts_ n).
We will prove u = v.
We prove the intermediate claim Luv: u ∩ SNoElts_ n = v ∩ SNoElts_ n.
An exact proof term for the current goal is Hf2 (u ∩ SNoElts_ n) Hu1 (v ∩ SNoElts_ n) Hv1 Hguv.
Apply SNo_eq u v Hu0a Hv0a to the current goal.
We will prove SNoLev u = SNoLev v.
rewrite the current goal using Hv0b (from left to right).
An exact proof term for the current goal is Hu0b.
We will prove SNoEq_ (SNoLev u) u v.
rewrite the current goal using Hu0b (from left to right).
We will prove SNoEq_ (ordsucc n) u v.
Let i be given.
Assume Hi: i ∈ ordsucc n.
Apply ordsuccE n i Hi to the current goal.
Assume H3: i ∈ n.
We will prove i ∈ u ↔ i ∈ v.
Apply iff_trans (i ∈ u) (i ∈ u ∩ SNoElts_ n) (i ∈ v) to the current goal.
We will prove i ∈ u ↔ i ∈ u ∩ SNoElts_ n.
Apply iff_sym to the current goal.
An exact proof term for the current goal is restr_SNoEq u ?? n LnLu i H3.
We will prove i ∈ u ∩ SNoElts_ n ↔ i ∈ v.
rewrite the current goal using Luv (from left to right).
We will prove i ∈ v ∩ SNoElts_ n ↔ i ∈ v.
An exact proof term for the current goal is restr_SNoEq v ?? n LnLv i H3.
Assume H3: i = n.
rewrite the current goal using H3 (from left to right).
Apply iffI to the current goal.
Assume _.
An exact proof term for the current goal is H2.
Assume _.
An exact proof term for the current goal is H1.
Assume H2: n ∉ v.
rewrite the current goal using Hg2 v H2 (from left to right).
Assume Hguv: f (u ∩ SNoElts_ n) = 2 ^ n + f (v ∩ SNoElts_ n).
We will prove False.
Apply SNoLt_irref (2 ^ n) to the current goal.
We will prove 2 ^ n < 2 ^ n.
Apply SNoLeLt_tra (2 ^ n) (2 ^ n + f (v ∩ SNoElts_ n)) (2 ^ n) L2n3 (SNo_add_SNo (2 ^ n) (f (v ∩ SNoElts_ n)) L2n3 Lfv3) L2n3 to the current goal.
We will prove 2 ^ n ≤ 2 ^ n + f (v ∩ SNoElts_ n).
rewrite the current goal using add_SNo_0R (2 ^ n) L2n3 (from right to left) at position 1.
We will prove 2 ^ n + 0 ≤ 2 ^ n + f (v ∩ SNoElts_ n).
Apply add_SNo_Le2 (2 ^ n) 0 (f (v ∩ SNoElts_ n)) L2n3 SNo_0 Lfv3 to the current goal.
We will prove 0 ≤ f (v ∩ SNoElts_ n).
An exact proof term for the current goal is omega_nonneg (f (v ∩ SNoElts_ n)) (nat_p_omega (f (v ∩ SNoElts_ n)) Lfv1).
We will prove 2 ^ n + f (v ∩ SNoElts_ n) < 2 ^ n.
rewrite the current goal using Hguv (from right to left).
An exact proof term for the current goal is Lfu4.
Assume H1: n ∉ u.
rewrite the current goal using Hg2 u H1 (from left to right).
Apply xm (n ∈ v) to the current goal.
Assume H2: n ∈ v.
rewrite the current goal using Hg1 v H2 (from left to right).
Assume Hguv: 2 ^ n + f (u ∩ SNoElts_ n) = f (v ∩ SNoElts_ n).
We will prove False.
Apply SNoLt_irref (2 ^ n) to the current goal.
We will prove 2 ^ n < 2 ^ n.
Apply SNoLeLt_tra (2 ^ n) (2 ^ n + f (u ∩ SNoElts_ n)) (2 ^ n) L2n3 (SNo_add_SNo (2 ^ n) (f (u ∩ SNoElts_ n)) L2n3 Lfu3) L2n3 to the current goal.
We will prove 2 ^ n ≤ 2 ^ n + f (u ∩ SNoElts_ n).
rewrite the current goal using add_SNo_0R (2 ^ n) L2n3 (from right to left) at position 1.
We will prove 2 ^ n + 0 ≤ 2 ^ n + f (u ∩ SNoElts_ n).
Apply add_SNo_Le2 (2 ^ n) 0 (f (u ∩ SNoElts_ n)) L2n3 SNo_0 Lfu3 to the current goal.
We will prove 0 ≤ f (u ∩ SNoElts_ n).
An exact proof term for the current goal is omega_nonneg (f (u ∩ SNoElts_ n)) (nat_p_omega (f (u ∩ SNoElts_ n)) Lfu1).
We will prove 2 ^ n + f (u ∩ SNoElts_ n) < 2 ^ n.
rewrite the current goal using Hguv (from left to right).
An exact proof term for the current goal is Lfv4.
Assume H2: n ∉ v.
rewrite the current goal using Hg2 v H2 (from left to right).
Assume Hguv: 2 ^ n + f (u ∩ SNoElts_ n) = 2 ^ n + f (v ∩ SNoElts_ n).
We will prove u = v.
We prove the intermediate claim Luv: u ∩ SNoElts_ n = v ∩ SNoElts_ n.
Apply Hf2 (u ∩ SNoElts_ n) Hu1 (v ∩ SNoElts_ n) Hv1 to the current goal.
We will prove f (u ∩ SNoElts_ n) = f (v ∩ SNoElts_ n).
An exact proof term for the current goal is add_SNo_cancel_L (2 ^ n) (f (u ∩ SNoElts_ n)) (f (v ∩ SNoElts_ n)) L2n3 Lfu3 Lfv3 Hguv.
Apply SNo_eq u v Hu0a Hv0a to the current goal.
We will prove SNoLev u = SNoLev v.
rewrite the current goal using Hv0b (from left to right).
An exact proof term for the current goal is Hu0b.
We will prove SNoEq_ (SNoLev u) u v.
rewrite the current goal using Hu0b (from left to right).
We will prove SNoEq_ (ordsucc n) u v.
Let i be given.
Assume Hi: i ∈ ordsucc n.
Apply ordsuccE n i Hi to the current goal.
Assume H3: i ∈ n.
We will prove i ∈ u ↔ i ∈ v.
Apply iff_trans (i ∈ u) (i ∈ u ∩ SNoElts_ n) (i ∈ v) to the current goal.
We will prove i ∈ u ↔ i ∈ u ∩ SNoElts_ n.
Apply iff_sym to the current goal.
An exact proof term for the current goal is restr_SNoEq u ?? n LnLu i H3.
We will prove i ∈ u ∩ SNoElts_ n ↔ i ∈ v.
rewrite the current goal using Luv (from left to right).
We will prove i ∈ v ∩ SNoElts_ n ↔ i ∈ v.
An exact proof term for the current goal is restr_SNoEq v ?? n LnLv i H3.
Assume H3: i = n.
rewrite the current goal using H3 (from left to right).
Apply iffI to the current goal.
Assume H4: n ∈ u.
We will prove False.
An exact proof term for the current goal is H1 H4.
Assume H4: n ∈ v.
We will prove False.
An exact proof term for the current goal is H2 H4.
We will prove ∀m ∈ 2 ^ n + 2 ^ n, ∃u ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}, g u = m.
Let m be given.
Assume Hm: m ∈ 2 ^ n + 2 ^ n.
We prove the intermediate claim Lm1: nat_p m.
An exact proof term for the current goal is nat_p_trans (2 ^ n + 2 ^ n) L2n2n1 m Hm.
We prove the intermediate claim Lm2: SNo m.
An exact proof term for the current goal is nat_p_SNo m Lm1.
Apply add_SNo_omega_In_cases m (2 ^ n) (nat_p_omega (2 ^ n) L2n1) (2 ^ n) L2n1 Hm to the current goal.
Assume H1: m ∈ 2 ^ n.
Apply Hf3 m H1 to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu1: u ∈ {x ∈ SNoS_ ω|SNoLev x = n}.
Assume Hu2: f u = m.
Apply SepE (SNoS_ ω) (λx ⇒ SNoLev x = n) u Hu1 to the current goal.
Assume Hu3: u ∈ SNoS_ ω.
Assume Hu4: SNoLev u = n.
Apply SNoS_E2 ω omega_ordinal u Hu3 to the current goal.
Assume Hu3a Hu3b Hu3c Hu3d.
We prove the intermediate claim Lu1: SNo (SNo_extend1 u).
An exact proof term for the current goal is SNo_extend1_SNo u ??.
We prove the intermediate claim Lu2: SNoLev (SNo_extend1 u) = ordsucc n.
rewrite the current goal using Hu4 (from right to left).
An exact proof term for the current goal is SNo_extend1_SNoLev u ??.
We prove the intermediate claim Lu3: n ∈ SNo_extend1 u.
rewrite the current goal using Hu4 (from right to left).
An exact proof term for the current goal is SNo_extend1_In u ??.
We use (SNo_extend1 u) to witness the existential quantifier.
Apply andI to the current goal.
We will prove SNo_extend1 u ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}.
Apply SepI to the current goal.
Apply SNoS_I ω omega_ordinal (SNo_extend1 u) (ordsucc n) to the current goal.
We will prove ordsucc n ∈ ω.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is nat_p_omega n Hn.
We will prove SNo_ (ordsucc n) (SNo_extend1 u).
rewrite the current goal using Hu4 (from right to left).
We will prove SNo_ (ordsucc (SNoLev u)) (SNo_extend1 u).
An exact proof term for the current goal is SNo_extend1_SNo_ u ??.
We will prove SNoLev (SNo_extend1 u) = ordsucc n.
An exact proof term for the current goal is Lu2.
We will prove g (SNo_extend1 u) = m.
rewrite the current goal using Hg1 (SNo_extend1 u) Lu3 (from left to right).
We will prove f (SNo_extend1 u ∩ SNoElts_ n) = m.
rewrite the current goal using Hu4 (from right to left).
We will prove f (SNo_extend1 u ∩ SNoElts_ (SNoLev u)) = m.
rewrite the current goal using SNo_extend1_restr_eq u Hu3c (from right to left).
An exact proof term for the current goal is Hu2.
Assume H1: m + - 2 ^ n ∈ 2 ^ n.
Apply Hf3 (m + - 2 ^ n) H1 to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu1: u ∈ {x ∈ SNoS_ ω|SNoLev x = n}.
Assume Hu2: f u = m + - 2 ^ n.
Apply SepE (SNoS_ ω) (λx ⇒ SNoLev x = n) u Hu1 to the current goal.
Assume Hu3: u ∈ SNoS_ ω.
Assume Hu4: SNoLev u = n.
Apply SNoS_E2 ω omega_ordinal u Hu3 to the current goal.
Assume Hu3a Hu3b Hu3c Hu3d.
We prove the intermediate claim Lu1: SNo (SNo_extend0 u).
An exact proof term for the current goal is SNo_extend0_SNo u ??.
We prove the intermediate claim Lu2: SNoLev (SNo_extend0 u) = ordsucc n.
rewrite the current goal using Hu4 (from right to left).
An exact proof term for the current goal is SNo_extend0_SNoLev u ??.
We prove the intermediate claim Lu3: n ∉ SNo_extend0 u.
rewrite the current goal using Hu4 (from right to left).
An exact proof term for the current goal is SNo_extend0_nIn u ??.
We use (SNo_extend0 u) to witness the existential quantifier.
Apply andI to the current goal.
We will prove SNo_extend0 u ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}.
Apply SepI to the current goal.
Apply SNoS_I ω omega_ordinal (SNo_extend0 u) (ordsucc n) to the current goal.
We will prove ordsucc n ∈ ω.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is nat_p_omega n Hn.
We will prove SNo_ (ordsucc n) (SNo_extend0 u).
rewrite the current goal using Hu4 (from right to left).
We will prove SNo_ (ordsucc (SNoLev u)) (SNo_extend0 u).
An exact proof term for the current goal is SNo_extend0_SNo_ u ??.
We will prove SNoLev (SNo_extend0 u) = ordsucc n.
An exact proof term for the current goal is Lu2.
We will prove g (SNo_extend0 u) = m.
rewrite the current goal using Hg2 (SNo_extend0 u) Lu3 (from left to right).
We will prove 2 ^ n + f (SNo_extend0 u ∩ SNoElts_ n) = m.
rewrite the current goal using Hu4 (from right to left) at position 2.
We will prove 2 ^ n + f (SNo_extend0 u ∩ SNoElts_ (SNoLev u)) = m.
rewrite the current goal using SNo_extend0_restr_eq u Hu3c (from right to left).
We will prove 2 ^ n + f u = m.
rewrite the current goal using Hu2 (from left to right).
We will prove 2 ^ n + (m + - 2 ^ n) = m.
rewrite the current goal using add_SNo_com (2 ^ n) (m + - 2 ^ n) L2n3 (SNo_add_SNo m (- 2 ^ n) Lm2 (SNo_minus_SNo (2 ^ n) L2n3)) (from left to right).
We will prove (m + - 2 ^ n) + 2 ^ n = m.
rewrite the current goal using add_SNo_assoc m (- 2 ^ n) (2 ^ n) Lm2 (SNo_minus_SNo (2 ^ n) L2n3) L2n3 (from right to left).
We will prove m + (- 2 ^ n + 2 ^ n) = m.
rewrite the current goal using add_SNo_minus_SNo_linv (2 ^ n) L2n3 (from left to right).
We will prove m + 0 = m.
An exact proof term for the current goal is add_SNo_0R m Lm2.
∎