Let X, x, n0, F0, e0, n, F and e be given.
Assume HxX: x ∈ X.
Assume Hn0O: n0 ∈ ω.
Assume HFfin: finite F.
Assume HF0subF: F0 ⊆ F.
Assume HF0ne: ∃f : set, f ∈ F0.
Assume HvalUI0: ∀f : set, f ∈ F0 → apply_fun f x ∈ unit_interval.
Assume HzeroOut: ∀f : set, f ∈ F → ¬ (f ∈ F0) → apply_fun f x = 0.
Assume Hbij0: bijection n0 F0 e0.
Assume HnO: n ∈ ω.
Assume Hbij: bijection n F e.
Set D to be the term F ∖ F0.
We prove the intermediate claim HDsubF: D ⊆ F.
An exact proof term for the current goal is (setminus_Subq F F0).
We prove the intermediate claim HDfin: finite D.
An exact proof term for the current goal is (Subq_finite F HFfin D HDsubF).
We prove the intermediate claim HDnotF0: ∀f : set, f ∈ D → ¬ (f ∈ F0).
Let f be given.
Assume HfD: f ∈ D.
An exact proof term for the current goal is (setminusE2 F F0 f HfD).
We prove the intermediate claim HzeroD: ∀f : set, f ∈ D → apply_fun f x = 0.
Let f be given.
Assume HfD: f ∈ D.
We prove the intermediate claim HfF: f ∈ F.
An exact proof term for the current goal is (setminusE1 F F0 f HfD).
An exact proof term for the current goal is (HzeroOut f HfF (HDnotF0 f HfD)).
We prove the intermediate claim HeqFD: F = F0 ∪ D.
Apply set_ext to the current goal.
Let u be given.
Assume HuF: u ∈ F.
Apply (xm (u ∈ F0)) to the current goal.
Assume HuF0: u ∈ F0.
An exact proof term for the current goal is (binunionI1 F0 D u HuF0).
Assume HnotF0: ¬ (u ∈ F0).
We prove the intermediate claim HuD: u ∈ D.
An exact proof term for the current goal is (setminusI F F0 u HuF HnotF0).
An exact proof term for the current goal is (binunionI2 F0 D u HuD).
Let u be given.
Assume HuU: u ∈ F0 ∪ D.
Apply (binunionE F0 D u HuU) to the current goal.
Assume HuF0: u ∈ F0.
An exact proof term for the current goal is (HF0subF u HuF0).
Assume HuD: u ∈ D.
An exact proof term for the current goal is (HDsubF u HuD).
We prove the intermediate claim HbijU: bijection n (F0 ∪ D) e.
rewrite the current goal using HeqFD (from right to left).
An exact proof term for the current goal is Hbij.
Set Pdrop to be the term λT : set ⇒ ∀nT eT : set, finite T → (∀f : set, f ∈ T → ¬ (f ∈ F0)) → (∀f : set, f ∈ T → apply_fun f x = 0) → nT ∈ ω → bijection nT (F0 ∪ T) eT → nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e0 k) x)) n0 = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eT k) x)) nT.
We prove the intermediate claim HP0: Pdrop Empty.
Let nT and eT be given.
Assume HTfin: finite Empty.
Assume HnotF0T: ∀f : set, f ∈ Empty → ¬ (f ∈ F0).
Assume HzeroT: ∀f : set, f ∈ Empty → apply_fun f x = 0.
Assume HnTO: nT ∈ ω.
Assume HbijT: bijection nT (F0 ∪ Empty) eT.
We prove the intermediate claim HeqU: (F0 ∪ Empty) = F0.
Apply set_ext to the current goal.
Let u be given.
Assume HuU: u ∈ F0 ∪ Empty.
Apply (binunionE F0 Empty u HuU) to the current goal.
Assume HuF0: u ∈ F0.
An exact proof term for the current goal is HuF0.
Assume HuE: u ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE u HuE).
Let u be given.
Assume HuF0: u ∈ F0.
An exact proof term for the current goal is (binunionI1 F0 Empty u HuF0).
We prove the intermediate claim HbijF0: bijection nT F0 eT.
rewrite the current goal using HeqU (from right to left).
An exact proof term for the current goal is HbijT.
We prove the intermediate claim Heq_n0F0: equip n0 F0.
An exact proof term for the current goal is (equip_of_bijection n0 F0 e0 Hbij0).
We prove the intermediate claim Heq_nTF0: equip nT F0.
An exact proof term for the current goal is (equip_of_bijection nT F0 eT HbijF0).
We prove the intermediate claim Heq_n0nT: equip n0 nT.
An exact proof term for the current goal is (equip_tra n0 F0 nT Heq_n0F0 (equip_sym nT F0 Heq_nTF0)).
We prove the intermediate claim Hn0Eq: n0 = nT.
An exact proof term for the current goal is (equip_omega_eq n0 nT Hn0O HnTO Heq_n0nT).
We prove the intermediate claim Hn0Nat: nat_p n0.
An exact proof term for the current goal is (omega_nat_p n0 Hn0O).
We prove the intermediate claim Hcase0: n0 = 0 ∨ ∃m0 : set, nat_p m0 ∧ n0 = ordsucc m0.
An exact proof term for the current goal is (nat_inv n0 Hn0Nat).
Apply (Hcase0 (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e0 k) x)) n0 = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eT k) x)) nT)) to the current goal.
Assume Hn00: n0 = 0.
Apply FalseE to the current goal.
Apply HF0ne to the current goal.
Let f be given.
Assume HfF0: f ∈ F0.
We prove the intermediate claim Hcod: f ∈ (F0 ∪ Empty).
An exact proof term for the current goal is (binunionI1 F0 Empty f HfF0).
We prove the intermediate claim HbijZ: bijection 0 (F0 ∪ Empty) eT.
rewrite the current goal using Hn00 (from right to left) at position 1.
rewrite the current goal using Hn0Eq (from left to right) at position 1.
An exact proof term for the current goal is HbijT.
We prove the intermediate claim Hexk: ∃k : set, k ∈ 0 ∧ apply_fun eT k = f.
An exact proof term for the current goal is (bijection_surj 0 (F0 ∪ Empty) eT f HbijZ Hcod).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpack.
An exact proof term for the current goal is (EmptyE k (andEL (k ∈ 0) (apply_fun eT k = f) Hkpack)).
Assume Hexm0: ∃m0 : set, nat_p m0 ∧ n0 = ordsucc m0.
Apply Hexm0 to the current goal.
Let m0 be given.
Assume Hm0pack: nat_p m0 ∧ n0 = ordsucc m0.
We prove the intermediate claim Hm0Nat: nat_p m0.
An exact proof term for the current goal is (andEL (nat_p m0) (n0 = ordsucc m0) Hm0pack).
We prove the intermediate claim Hn0Sm0: n0 = ordsucc m0.
An exact proof term for the current goal is (andER (nat_p m0) (n0 = ordsucc m0) Hm0pack).
We prove the intermediate claim Hm0O: m0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega m0 Hm0Nat).
We prove the intermediate claim HnTSm0: nT = ordsucc m0.
rewrite the current goal using Hn0Eq (from right to left).
An exact proof term for the current goal is Hn0Sm0.
We prove the intermediate claim Hbij0': bijection (ordsucc m0) F0 e0.
rewrite the current goal using Hn0Sm0 (from right to left).
An exact proof term for the current goal is Hbij0.
We prove the intermediate claim HbijT': bijection (ordsucc m0) F0 eT.
rewrite the current goal using HnTSm0 (from right to left).
An exact proof term for the current goal is HbijF0.
rewrite the current goal using Hn0Sm0 (from left to right) at position 1.
rewrite the current goal using HnTSm0 (from left to right) at position 1.
An exact proof term for the current goal is (nat_primrec_sum_bijection_independent_unit_interval X m0 F0 e0 eT x Hm0O HxX Hbij0' HbijT' HvalUI0).
We prove the intermediate claim HPS: ∀T y : set, finite T → y ∉ T → Pdrop T → Pdrop (T ∪ {y}).
Let T and y be given.
Assume HTfin: finite T.
Assume HyNot: y ∉ T.
Assume IH: Pdrop T.
We will prove Pdrop (T ∪ {y}).
Let nT and eT be given.
Assume HTyfin: finite (T ∪ {y}).
Assume HnotF0Ty: ∀f : set, f ∈ (T ∪ {y}) → ¬ (f ∈ F0).
Assume HzeroTy: ∀f : set, f ∈ (T ∪ {y}) → apply_fun f x = 0.
Assume HnTO: nT ∈ ω.
Assume HbijTy: bijection nT (F0 ∪ (T ∪ {y})) eT.
We prove the intermediate claim HyNotF0: ¬ (y ∈ F0).
An exact proof term for the current goal is (HnotF0Ty y (binunionI2 T {y} y (SingI y))).
We prove the intermediate claim Hy0: apply_fun y x = 0.
An exact proof term for the current goal is (HzeroTy y (binunionI2 T {y} y (SingI y))).
We prove the intermediate claim HnTnat: nat_p nT.
An exact proof term for the current goal is (omega_nat_p nT HnTO).
We prove the intermediate claim Hcase: nT = 0 ∨ ∃m : set, nat_p m ∧ nT = ordsucc m.
An exact proof term for the current goal is (nat_inv nT HnTnat).
Apply (Hcase (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e0 k) x)) n0 = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eT k) x)) nT)) to the current goal.
Assume Hn0: nT = 0.
Apply FalseE to the current goal.
Apply HF0ne to the current goal.
Let f be given.
Assume HfF0: f ∈ F0.
We prove the intermediate claim Hcod: f ∈ (F0 ∪ (T ∪ {y})).
An exact proof term for the current goal is (binunionI1 F0 (T ∪ {y}) f HfF0).
We prove the intermediate claim Hbij0Ty: bijection 0 (F0 ∪ (T ∪ {y})) eT.
rewrite the current goal using Hn0 (from right to left).
An exact proof term for the current goal is HbijTy.
We prove the intermediate claim Hexk: ∃k : set, k ∈ 0 ∧ apply_fun eT k = f.
An exact proof term for the current goal is (bijection_surj 0 (F0 ∪ (T ∪ {y})) eT f Hbij0Ty Hcod).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpack.
An exact proof term for the current goal is (EmptyE k (andEL (k ∈ 0) (apply_fun eT k = f) Hkpack)).
Assume Hexm: ∃m : set, nat_p m ∧ nT = ordsucc m.
Apply Hexm to the current goal.
Let m be given.
Assume Hmpack: nat_p m ∧ nT = ordsucc m.
We prove the intermediate claim HmNat: nat_p m.
An exact proof term for the current goal is (andEL (nat_p m) (nT = ordsucc m) Hmpack).
We prove the intermediate claim HnTEq: nT = ordsucc m.
An exact proof term for the current goal is (andER (nat_p m) (nT = ordsucc m) Hmpack).
We prove the intermediate claim HmO: m ∈ ω.
An exact proof term for the current goal is (nat_p_omega m HmNat).
We prove the intermediate claim HyInCod: y ∈ (F0 ∪ (T ∪ {y})).
An exact proof term for the current goal is (binunionI2 F0 (T ∪ {y}) y (binunionI2 T {y} y (SingI y))).
We prove the intermediate claim HtermUI_all: ∀f : set, f ∈ (F0 ∪ (T ∪ {y})) → apply_fun f x ∈ unit_interval.
Let f be given.
Assume HfU: f ∈ (F0 ∪ (T ∪ {y})).
Apply (binunionE F0 (T ∪ {y}) f HfU) to the current goal.
Assume HfF0: f ∈ F0.
An exact proof term for the current goal is (HvalUI0 f HfF0).
Assume HfT: f ∈ (T ∪ {y}).
We prove the intermediate claim Hfx0: apply_fun f x = 0.
An exact proof term for the current goal is (HzeroTy f HfT).
rewrite the current goal using Hfx0 (from left to right).
An exact proof term for the current goal is zero_in_unit_interval.
We prove the intermediate claim HbijTyS: bijection (ordsucc m) (F0 ∪ (T ∪ {y})) eT.
rewrite the current goal using HnTEq (from right to left).
An exact proof term for the current goal is HbijTy.
We prove the intermediate claim Hdrop: ∃e' : set, bijection m ((F0 ∪ (T ∪ {y})) ∖ {y}) e' ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eT k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e' k) x)) m.
An exact proof term for the current goal is (nat_primrec_sum_bijection_drop_zero_element_unit_interval X m (F0 ∪ (T ∪ {y})) eT y x HmO HxX HbijTyS HyInCod HtermUI_all Hy0).
Apply Hdrop to the current goal.
Let e' be given.
Assume He'pack.
We prove the intermediate claim HbijDrop: bijection m ((F0 ∪ (T ∪ {y})) ∖ {y}) e'.
An exact proof term for the current goal is (andEL (bijection m ((F0 ∪ (T ∪ {y})) ∖ {y}) e') (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eT k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e' k) x)) m) He'pack).
We prove the intermediate claim HsumDrop: nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eT k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e' k) x)) m.
An exact proof term for the current goal is (andER (bijection m ((F0 ∪ (T ∪ {y})) ∖ {y}) e') (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eT k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e' k) x)) m) He'pack).
We prove the intermediate claim HeqSet: ((F0 ∪ (T ∪ {y})) ∖ {y}) = (F0 ∪ T).
Apply set_ext to the current goal.
Let u be given.
Assume Hu: u ∈ ((F0 ∪ (T ∪ {y})) ∖ {y}).
We prove the intermediate claim HuU: u ∈ (F0 ∪ (T ∪ {y})).
An exact proof term for the current goal is (setminusE1 (F0 ∪ (T ∪ {y})) {y} u Hu).
We prove the intermediate claim HuNy: u ∉ {y}.
An exact proof term for the current goal is (setminusE2 (F0 ∪ (T ∪ {y})) {y} u Hu).
Apply (binunionE F0 (T ∪ {y}) u HuU) to the current goal.
Assume HuF0: u ∈ F0.
An exact proof term for the current goal is (binunionI1 F0 T u HuF0).
Assume HuT0: u ∈ (T ∪ {y}).
Apply (binunionE T {y} u HuT0) to the current goal.
Assume HuT: u ∈ T.
An exact proof term for the current goal is (binunionI2 F0 T u HuT).
Assume Huy: u ∈ {y}.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HuNy Huy).
Let u be given.
Assume Hu: u ∈ (F0 ∪ T).
Apply (binunionE F0 T u Hu) to the current goal.
Assume HuF0: u ∈ F0.
We prove the intermediate claim HuU: u ∈ (F0 ∪ (T ∪ {y})).
An exact proof term for the current goal is (binunionI1 F0 (T ∪ {y}) u HuF0).
We prove the intermediate claim HuNy: u ∉ {y}.
Assume Huy: u ∈ {y}.
We prove the intermediate claim Hueq: u = y.
An exact proof term for the current goal is (SingE y u Huy).
Apply HyNotF0 to the current goal.
rewrite the current goal using Hueq (from right to left).
An exact proof term for the current goal is HuF0.
An exact proof term for the current goal is (setminusI (F0 ∪ (T ∪ {y})) {y} u HuU HuNy).
Assume HuT: u ∈ T.
We prove the intermediate claim HuU: u ∈ (F0 ∪ (T ∪ {y})).
An exact proof term for the current goal is (binunionI2 F0 (T ∪ {y}) u (binunionI1 T {y} u HuT)).
We prove the intermediate claim HuNy: u ∉ {y}.
Assume Huy: u ∈ {y}.
We prove the intermediate claim Hueq: u = y.
An exact proof term for the current goal is (SingE y u Huy).
Apply HyNot to the current goal.
rewrite the current goal using Hueq (from right to left).
An exact proof term for the current goal is HuT.
An exact proof term for the current goal is (setminusI (F0 ∪ (T ∪ {y})) {y} u HuU HuNy).
We prove the intermediate claim HbijDrop2: bijection m (F0 ∪ T) e'.
rewrite the current goal using HeqSet (from right to left).
An exact proof term for the current goal is HbijDrop.
We prove the intermediate claim HTfin2: finite T.
An exact proof term for the current goal is HTfin.
We prove the intermediate claim HnotF0T2: ∀f : set, f ∈ T → ¬ (f ∈ F0).
Let f be given.
Assume HfT: f ∈ T.
An exact proof term for the current goal is (HnotF0Ty f (binunionI1 T {y} f HfT)).
We prove the intermediate claim HzeroT2: ∀f : set, f ∈ T → apply_fun f x = 0.
Let f be given.
Assume HfT: f ∈ T.
An exact proof term for the current goal is (HzeroTy f (binunionI1 T {y} f HfT)).
We prove the intermediate claim HmO2: m ∈ ω.
An exact proof term for the current goal is (nat_p_omega m HmNat).
We prove the intermediate claim Hind: nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e0 k) x)) n0 = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e' k) x)) m.
An exact proof term for the current goal is (IH m e' HTfin2 HnotF0T2 HzeroT2 HmO2 HbijDrop2).
rewrite the current goal using HnTEq (from left to right) at position 1.
rewrite the current goal using HsumDrop (from left to right) at position 1.
An exact proof term for the current goal is Hind.
We prove the intermediate claim HPdropD: Pdrop D.
An exact proof term for the current goal is (finite_ind Pdrop HP0 HPS D HDfin).
An exact proof term for the current goal is (HPdropD n e HDfin HDnotF0 HzeroD HnO HbijU).
∎