Let F0, ea and eb be given.

Assume H0O: 0 ∈ ω.

Assume Hba: bijection (ordsucc 0) F0 ea.

Assume Hbb: bijection (ordsucc 0) F0 eb.

Assume _: ∀f : set, f ∈ F0 → apply_fun f x ∈ unit_interval.

We prove the intermediate claim HeaFun: function_on ea (ordsucc 0) F0.

An exact proof term for the current goal is (andEL (function_on ea (ordsucc 0) F0) (∀y : set, y ∈ F0 → ∃k0 : set, k0 ∈ ordsucc 0 ∧ apply_fun ea k0 = y ∧ (∀k' : set, k' ∈ ordsucc 0 → apply_fun ea k' = y → k' = k0)) Hba).

We prove the intermediate claim Hea0F0: apply_fun ea 0 ∈ F0.

An exact proof term for the current goal is (HeaFun 0 (ordsuccI2 0)).

We prove the intermediate claim HebSurj: ∀y : set, y ∈ F0 → ∃k0 : set, k0 ∈ ordsucc 0 ∧ apply_fun eb k0 = y ∧ (∀k' : set, k' ∈ ordsucc 0 → apply_fun eb k' = y → k' = k0).

An exact proof term for the current goal is (andER (function_on eb (ordsucc 0) F0) (∀y : set, y ∈ F0 → ∃k0 : set, k0 ∈ ordsucc 0 ∧ apply_fun eb k0 = y ∧ (∀k' : set, k' ∈ ordsucc 0 → apply_fun eb k' = y → k' = k0)) Hbb).

Apply (HebSurj (apply_fun ea 0) Hea0F0) to the current goal.

Let k0 be given.

Assume Hk0pack.

We prove the intermediate claim Hk0left: k0 ∈ ordsucc 0 ∧ apply_fun eb k0 = apply_fun ea 0.

An exact proof term for the current goal is (andEL (k0 ∈ ordsucc 0 ∧ apply_fun eb k0 = apply_fun ea 0) (∀k' : set, k' ∈ ordsucc 0 → apply_fun eb k' = apply_fun ea 0 → k' = k0) Hk0pack).

We prove the intermediate claim Hk0In: k0 ∈ ordsucc 0.

An exact proof term for the current goal is (andEL (k0 ∈ ordsucc 0) (apply_fun eb k0 = apply_fun ea 0) Hk0left).

We prove the intermediate claim HebEq: apply_fun eb k0 = apply_fun ea 0.

An exact proof term for the current goal is (andER (k0 ∈ ordsucc 0) (apply_fun eb k0 = apply_fun ea 0) Hk0left).

We prove the intermediate claim Hk0eq0: k0 = 0.

We prove the intermediate claim Hk0Case: k0 ∈ 0 ∨ k0 = 0.

An exact proof term for the current goal is (ordsuccE 0 k0 Hk0In).

Apply (Hk0Case (k0 = 0)) to the current goal.

Assume Hk0E: k0 ∈ 0.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE k0 Hk0E).

Assume Hk0Z: k0 = 0.

An exact proof term for the current goal is Hk0Z.

We prove the intermediate claim Heb0Eq: apply_fun eb 0 = apply_fun ea 0.

rewrite the current goal using Hk0eq0 (from right to left) at position 1.

An exact proof term for the current goal is HebEq.

We prove the intermediate claim H0Nat: nat_p 0.

An exact proof term for the current goal is (omega_nat_p 0 H0O).

rewrite the current goal using (nat_primrec_S 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun ea k) x)) 0 H0Nat) (from left to right).

rewrite the current goal using (nat_primrec_S 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb k) x)) 0 H0Nat) (from left to right).

rewrite the current goal using (nat_primrec_0 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun ea k) x))) (from left to right).

rewrite the current goal using (nat_primrec_0 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb k) x))) (from left to right).

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

Use reflexivity.

Let t be given.

Assume HtNat: nat_p t.

Assume IHt: Pm t.

We will prove Pm (ordsucc t).

Let F0, ea and eb be given.

Assume HnO: ordsucc t ∈ ω.

Assume Hba: bijection (ordsucc (ordsucc t)) F0 ea.

Assume Hbb: bijection (ordsucc (ordsucc t)) F0 eb.

Assume HUI: ∀f : set, f ∈ F0 → apply_fun f x ∈ unit_interval.

Set n to be the term ordsucc t.

We prove the intermediate claim HnDef: n = ordsucc t.

Use reflexivity.

We prove the intermediate claim HtO: t ∈ ω.

An exact proof term for the current goal is (nat_p_omega t HtNat).

We prove the intermediate claim HnNat: nat_p n.

An exact proof term for the current goal is (omega_nat_p n HnO).

Set flast to be the term apply_fun ea n.

We prove the intermediate claim HeaFun: function_on ea (ordsucc n) F0.

An exact proof term for the current goal is (andEL (function_on ea (ordsucc n) F0) (∀y : set, y ∈ F0 → ∃k0 : set, k0 ∈ ordsucc n ∧ apply_fun ea k0 = y ∧ (∀k' : set, k' ∈ ordsucc n → apply_fun ea k' = y → k' = k0)) Hba).

We prove the intermediate claim HflF0: flast ∈ F0.

An exact proof term for the current goal is (HeaFun n (ordsuccI2 n)).

We prove the intermediate claim Hmove: ∃eb' : set, bijection (ordsucc n) F0 eb' ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb k) x)) (ordsucc n) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb' k) x)) (ordsucc n) ∧ apply_fun eb' n = flast.

An exact proof term for the current goal is (nat_primrec_sum_bijection_move_value_to_last_unit_interval X n F0 eb flast x HnO HxX Hbb HflF0 HUI).

Apply Hmove to the current goal.

Let eb' be given.

Assume Heb'pack.

We prove the intermediate claim Heb'left: bijection (ordsucc n) F0 eb' ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb k) x)) (ordsucc n) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb' k) x)) (ordsucc n).

An exact proof term for the current goal is (andEL (bijection (ordsucc n) F0 eb' ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb k) x)) (ordsucc n) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb' k) x)) (ordsucc n)) (apply_fun eb' n = flast) Heb'pack).

We prove the intermediate claim HbijB: bijection (ordsucc n) F0 eb'.

An exact proof term for the current goal is (andEL (bijection (ordsucc n) F0 eb') (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb k) x)) (ordsucc n) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb' k) x)) (ordsucc n)) Heb'left).

We prove the intermediate claim HsumB: nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb k) x)) (ordsucc n) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb' k) x)) (ordsucc n).

An exact proof term for the current goal is (andER (bijection (ordsucc n) F0 eb') (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb k) x)) (ordsucc n) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb' k) x)) (ordsucc n)) Heb'left).

We prove the intermediate claim Heb'Last: apply_fun eb' n = flast.

An exact proof term for the current goal is (andER (bijection (ordsucc n) F0 eb' ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb k) x)) (ordsucc n) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb' k) x)) (ordsucc n)) (apply_fun eb' n = flast) Heb'pack).

We prove the intermediate claim HdropA: bijection n (F0 ∖ {flast}) ea.

An exact proof term for the current goal is (bijection_drop_last n F0 ea HnO Hba).

We prove the intermediate claim HdropB: bijection n (F0 ∖ {flast}) eb'.

We prove the intermediate claim HlastEq: apply_fun eb' n = flast.

An exact proof term for the current goal is Heb'Last.

rewrite the current goal using HlastEq (from right to left) at position 1.

An exact proof term for the current goal is (bijection_drop_last n F0 eb' HnO HbijB).

We prove the intermediate claim HUI_drop: ∀f : set, f ∈ (F0 ∖ {flast}) → apply_fun f x ∈ unit_interval.

Let f be given.

Assume Hf: f ∈ (F0 ∖ {flast}).

An exact proof term for the current goal is (HUI f (setminusE1 F0 {flast} f Hf)).

We prove the intermediate claim HprefixEq: nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun ea k) x)) n = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb' k) x)) n.

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

An exact proof term for the current goal is (IHt (F0 ∖ {flast}) ea eb' HtO HdropA HdropB HUI_drop).

We prove the intermediate claim HlastTermEq: apply_fun (apply_fun ea n) x = apply_fun (apply_fun eb' n) x.

rewrite the current goal using Heb'Last (from left to right).

Use reflexivity.

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

rewrite the current goal using (nat_primrec_S 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun ea k) x)) n HnNat) (from left to right).

rewrite the current goal using (nat_primrec_S 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb' k) x)) n HnNat) (from left to right).

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

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

Use reflexivity.