Let X, m, F, e, flast and x be given.
Assume HmO: m ∈ ω.
Assume HxX: x ∈ X.
Assume Hbij: bijection (ordsucc m) F e.
Assume HflF: flast ∈ F.
Assume HvalUI: ∀f : set, f ∈ F → apply_fun f x ∈ unit_interval.
We prove the intermediate claim HmNat: nat_p m.
An exact proof term for the current goal is (omega_nat_p m HmO).
Set step to be the term (λe0 : set ⇒ λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e0 k) x)).
Set Pm to be the term (λm0 : set ⇒ ∀F0 e0 fl0 : set, m0 ∈ ω → bijection (ordsucc m0) F0 e0 → fl0 ∈ F0 → (∀f : set, f ∈ F0 → apply_fun f x ∈ unit_interval) → ∃e' : set, bijection (ordsucc m0) F0 e' ∧ nat_primrec 0 (step e0) (ordsucc m0) = nat_primrec 0 (step e') (ordsucc m0) ∧ apply_fun e' m0 = fl0).
We prove the intermediate claim HP0: Pm 0.
Let F0, e0 and fl0 be given.
Assume H0O: 0 ∈ ω.
Assume Hbij0: bijection (ordsucc 0) F0 e0.
Assume Hfl0: fl0 ∈ F0.
Assume HvalUI0: ∀f : set, f ∈ F0 → apply_fun f x ∈ unit_interval.
We use e0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hbij0.
Use reflexivity.
We prove the intermediate claim Hsurj: ∃k : set, k ∈ ordsucc 0 ∧ apply_fun e0 k = fl0 ∧ (∀k' : set, k' ∈ ordsucc 0 → apply_fun e0 k' = fl0 → k' = k).
Apply Hbij0 to the current goal.
Assume _ Huniq.
An exact proof term for the current goal is (Huniq fl0 Hfl0).
Apply Hsurj to the current goal.
Let k be given.
Assume Hkpack.
We prove the intermediate claim HkLeft: k ∈ ordsucc 0 ∧ apply_fun e0 k = fl0.
An exact proof term for the current goal is (andEL (k ∈ ordsucc 0 ∧ apply_fun e0 k = fl0) (∀k' : set, k' ∈ ordsucc 0 → apply_fun e0 k' = fl0 → k' = k) Hkpack).
We prove the intermediate claim HkIn: k ∈ ordsucc 0.
An exact proof term for the current goal is (andEL (k ∈ ordsucc 0) (apply_fun e0 k = fl0) HkLeft).
We prove the intermediate claim HkEq: apply_fun e0 k = fl0.
An exact proof term for the current goal is (andER (k ∈ ordsucc 0) (apply_fun e0 k = fl0) HkLeft).
We prove the intermediate claim HkCase: k ∈ 0 ∨ k = 0.
An exact proof term for the current goal is (ordsuccE 0 k HkIn).
We prove the intermediate claim Hk0: k = 0.
Apply (HkCase (k = 0)) to the current goal.
Assume HkIn0: k ∈ 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE k HkIn0).
Assume HkEq0: k = 0.
An exact proof term for the current goal is HkEq0.
rewrite the current goal using Hk0 (from right to left) at position 1.
An exact proof term for the current goal is HkEq.
We prove the intermediate claim HPS: ∀t : set, nat_p t → Pm t → Pm (ordsucc t).
Let t be given.
Assume HtNat: nat_p t.
Assume IHt: Pm t.
We will prove Pm (ordsucc t).
Let F0, e0 and fl0 be given.
Assume Hm1O: ordsucc t ∈ ω.
Assume HbijS: bijection (ordsucc (ordsucc t)) F0 e0.
Assume Hfl0: fl0 ∈ F0.
Assume HvalUI0: ∀f : set, f ∈ F0 → apply_fun f x ∈ unit_interval.
Set m1 to be the term ordsucc t.
We prove the intermediate claim Hm1Def: m1 = 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 Hm1Nat: nat_p m1.
rewrite the current goal using Hm1Def (from left to right).
An exact proof term for the current goal is (nat_ordsucc t HtNat).
We prove the intermediate claim Hm1O2: m1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega m1 Hm1Nat).
Set lastval to be the term apply_fun e0 m1.
We prove the intermediate claim He0fun: function_on e0 (ordsucc m1) F0.
An exact proof term for the current goal is (andEL (function_on e0 (ordsucc m1) F0) (∀y : set, y ∈ F0 → ∃x0 : set, x0 ∈ ordsucc m1 ∧ apply_fun e0 x0 = y ∧ (∀x' : set, x' ∈ ordsucc m1 → apply_fun e0 x' = y → x' = x0)) HbijS).
We prove the intermediate claim HlastF0: lastval ∈ F0.
An exact proof term for the current goal is (He0fun m1 (ordsuccI2 m1)).
Apply (xm (fl0 = lastval)) to the current goal.
Assume HeqLast: fl0 = lastval.
We use e0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HbijS.
Use reflexivity.
rewrite the current goal using HeqLast (from left to right).
Use reflexivity.
Assume HneqLast: ¬ (fl0 = lastval).
We prove the intermediate claim HflNot: fl0 ∉ {lastval}.
Assume Hmem: fl0 ∈ {lastval}.
We prove the intermediate claim Heq: fl0 = lastval.
An exact proof term for the current goal is (SingE lastval fl0 Hmem).
An exact proof term for the current goal is (HneqLast Heq).
We prove the intermediate claim HflInDrop: fl0 ∈ (F0 ∖ {lastval}).
An exact proof term for the current goal is (setminusI F0 {lastval} fl0 Hfl0 HflNot).
We prove the intermediate claim HbijDrop: bijection m1 (F0 ∖ {apply_fun e0 m1}) e0.
rewrite the current goal using Hm1Def (from right to left).
An exact proof term for the current goal is (bijection_drop_last m1 F0 e0 Hm1O2 HbijS).
We prove the intermediate claim HbijDrop2: bijection m1 (F0 ∖ {lastval}) e0.
We prove the intermediate claim HlastEq: apply_fun e0 m1 = lastval.
Use reflexivity.
rewrite the current goal using HlastEq (from right to left) at position 1.
An exact proof term for the current goal is HbijDrop.
We prove the intermediate claim HvalUIDrop: ∀f : set, f ∈ (F0 ∖ {lastval}) → apply_fun f x ∈ unit_interval.
Let f be given.
Assume Hf: f ∈ (F0 ∖ {lastval}).
An exact proof term for the current goal is (HvalUI0 f (setminusE1 F0 {lastval} f Hf)).
We prove the intermediate claim HmoveSmall: ∃e1 : set, bijection (ordsucc t) (F0 ∖ {lastval}) e1 ∧ nat_primrec 0 (step e0) (ordsucc t) = nat_primrec 0 (step e1) (ordsucc t) ∧ apply_fun e1 t = fl0.
An exact proof term for the current goal is (IHt (F0 ∖ {lastval}) e0 fl0 HtO HbijDrop2 HflInDrop HvalUIDrop).
Apply HmoveSmall to the current goal.
Let e1 be given.
Assume He1pack.
We prove the intermediate claim He1left: bijection (ordsucc t) (F0 ∖ {lastval}) e1 ∧ nat_primrec 0 (step e0) (ordsucc t) = nat_primrec 0 (step e1) (ordsucc t).
An exact proof term for the current goal is (andEL (bijection (ordsucc t) (F0 ∖ {lastval}) e1 ∧ nat_primrec 0 (step e0) (ordsucc t) = nat_primrec 0 (step e1) (ordsucc t)) (apply_fun e1 t = fl0) He1pack).
We prove the intermediate claim Hbij1: bijection (ordsucc t) (F0 ∖ {lastval}) e1.
An exact proof term for the current goal is (andEL (bijection (ordsucc t) (F0 ∖ {lastval}) e1) (nat_primrec 0 (step e0) (ordsucc t) = nat_primrec 0 (step e1) (ordsucc t)) He1left).
We prove the intermediate claim HsumSmall: nat_primrec 0 (step e0) (ordsucc t) = nat_primrec 0 (step e1) (ordsucc t).
An exact proof term for the current goal is (andER (bijection (ordsucc t) (F0 ∖ {lastval}) e1) (nat_primrec 0 (step e0) (ordsucc t) = nat_primrec 0 (step e1) (ordsucc t)) He1left).
We prove the intermediate claim He1last: apply_fun e1 t = fl0.
An exact proof term for the current goal is (andER (bijection (ordsucc t) (F0 ∖ {lastval}) e1 ∧ nat_primrec 0 (step e0) (ordsucc t) = nat_primrec 0 (step e1) (ordsucc t)) (apply_fun e1 t = fl0) He1pack).
Set e2 to be the term graph (ordsucc m1) (λk : set ⇒ If_i (k = m1) lastval (apply_fun e1 k)).
We prove the intermediate claim He2m1: apply_fun e2 m1 = lastval.
rewrite the current goal using (apply_fun_graph (ordsucc m1) (λk : set ⇒ If_i (k = m1) lastval (apply_fun e1 k)) m1 (ordsuccI2 m1)) (from left to right).
We prove the intermediate claim Hrefl: m1 = m1.
Use reflexivity.
rewrite the current goal using (If_i_1 (m1 = m1) lastval (apply_fun e1 m1) Hrefl) (from left to right).
Use reflexivity.
We prove the intermediate claim Hbij2: bijection (ordsucc m1) F0 e2.
We will prove function_on e2 (ordsucc m1) F0 ∧ ∀y : set, y ∈ F0 → ∃k0 : set, k0 ∈ ordsucc m1 ∧ apply_fun e2 k0 = y ∧ (∀k' : set, k' ∈ ordsucc m1 → apply_fun e2 k' = y → k' = k0).
Apply andI to the current goal.
Let k be given.
Assume HkDom: k ∈ ordsucc m1.
rewrite the current goal using (apply_fun_graph (ordsucc m1) (λk0 : set ⇒ If_i (k0 = m1) lastval (apply_fun e1 k0)) k HkDom) (from left to right).
Apply (xm (k = m1)) to the current goal.
Assume Hkm1: k = m1.
rewrite the current goal using (If_i_1 (k = m1) lastval (apply_fun e1 k) Hkm1) (from left to right).
An exact proof term for the current goal is HlastF0.
Assume Hknm1: ¬ (k = m1).
rewrite the current goal using (If_i_0 (k = m1) lastval (apply_fun e1 k) Hknm1) (from left to right).
We prove the intermediate claim HkInM1: k ∈ m1.
Apply (ordsuccE m1 k HkDom) to the current goal.
Assume HkM1: k ∈ m1.
An exact proof term for the current goal is HkM1.
Assume Hkeq: k = m1.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hknm1 Hkeq).
We prove the intermediate claim He1fun: function_on e1 m1 (F0 ∖ {lastval}).
An exact proof term for the current goal is (andEL (function_on e1 m1 (F0 ∖ {lastval})) (∀y : set, y ∈ (F0 ∖ {lastval}) → ∃x0 : set, x0 ∈ m1 ∧ apply_fun e1 x0 = y ∧ (∀x' : set, x' ∈ m1 → apply_fun e1 x' = y → x' = x0)) Hbij1).
We prove the intermediate claim He1kDrop: apply_fun e1 k ∈ (F0 ∖ {lastval}).
An exact proof term for the current goal is (He1fun k HkInM1).
An exact proof term for the current goal is (setminusE1 F0 {lastval} (apply_fun e1 k) He1kDrop).
Let y be given.
Assume HyF0: y ∈ F0.
Apply (xm (y = lastval)) to the current goal.
Assume HyLast: y = lastval.
We use m1 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (ordsuccI2 m1).
rewrite the current goal using HyLast (from left to right).
An exact proof term for the current goal is He2m1.
Let k' be given.
Assume Hk'Dom: k' ∈ ordsucc m1.
Assume Heq: apply_fun e2 k' = y.
Apply (xm (k' = m1)) to the current goal.
Assume H: k' = m1.
An exact proof term for the current goal is H.
Assume Hkn: ¬ (k' = m1).
We prove the intermediate claim HkInM1: k' ∈ m1.
Apply (ordsuccE m1 k' Hk'Dom) to the current goal.
Assume HkM1: k' ∈ m1.
An exact proof term for the current goal is HkM1.
Assume Hkeq: k' = m1.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hkn Hkeq).
We prove the intermediate claim He1fun: function_on e1 m1 (F0 ∖ {lastval}).
An exact proof term for the current goal is (andEL (function_on e1 m1 (F0 ∖ {lastval})) (∀y0 : set, y0 ∈ (F0 ∖ {lastval}) → ∃x0 : set, x0 ∈ m1 ∧ apply_fun e1 x0 = y0 ∧ (∀x' : set, x' ∈ m1 → apply_fun e1 x' = y0 → x' = x0)) Hbij1).
We prove the intermediate claim He1kDrop: apply_fun e1 k' ∈ (F0 ∖ {lastval}).
An exact proof term for the current goal is (He1fun k' HkInM1).
We prove the intermediate claim Hnot: apply_fun e1 k' ∉ {lastval}.
An exact proof term for the current goal is (setminusE2 F0 {lastval} (apply_fun e1 k') He1kDrop).
We prove the intermediate claim He2k: apply_fun e2 k' = apply_fun e1 k'.
rewrite the current goal using (apply_fun_graph (ordsucc m1) (λk0 : set ⇒ If_i (k0 = m1) lastval (apply_fun e1 k0)) k' Hk'Dom) (from left to right).
rewrite the current goal using (If_i_0 (k' = m1) lastval (apply_fun e1 k') Hkn) (from left to right).
Use reflexivity.
We prove the intermediate claim He1eqLast: apply_fun e1 k' = lastval.
We will prove apply_fun e1 k' = lastval.
rewrite the current goal using HyLast (from right to left).
rewrite the current goal using He2k (from right to left).
An exact proof term for the current goal is Heq.
We prove the intermediate claim Hmem: apply_fun e1 k' ∈ {lastval}.
rewrite the current goal using He1eqLast (from left to right).
An exact proof term for the current goal is (SingI lastval).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnot Hmem).
Assume HyNLast: ¬ (y = lastval).
We prove the intermediate claim HyDrop: y ∈ (F0 ∖ {lastval}).
An exact proof term for the current goal is (setminusI F0 {lastval} y HyF0 (λHyS : y ∈ {lastval} ⇒ HyNLast (SingE lastval y HyS))).
We prove the intermediate claim Hsurj1: ∃k0 : set, k0 ∈ m1 ∧ apply_fun e1 k0 = y ∧ (∀k' : set, k' ∈ m1 → apply_fun e1 k' = y → k' = k0).
Apply Hbij1 to the current goal.
Assume _ Huniq.
An exact proof term for the current goal is (Huniq y HyDrop).
Apply Hsurj1 to the current goal.
Let k0 be given.
Assume Hk0pack.
We prove the intermediate claim Hk0left: k0 ∈ m1 ∧ apply_fun e1 k0 = y.
An exact proof term for the current goal is (andEL (k0 ∈ m1 ∧ apply_fun e1 k0 = y) (∀k' : set, k' ∈ m1 → apply_fun e1 k' = y → k' = k0) Hk0pack).
We prove the intermediate claim Hk0In: k0 ∈ m1.
An exact proof term for the current goal is (andEL (k0 ∈ m1) (apply_fun e1 k0 = y) Hk0left).
We prove the intermediate claim Hk0Eq: apply_fun e1 k0 = y.
An exact proof term for the current goal is (andER (k0 ∈ m1) (apply_fun e1 k0 = y) Hk0left).
We prove the intermediate claim Hk0uniq: ∀k' : set, k' ∈ m1 → apply_fun e1 k' = y → k' = k0.
An exact proof term for the current goal is (andER (k0 ∈ m1 ∧ apply_fun e1 k0 = y) (∀k' : set, k' ∈ m1 → apply_fun e1 k' = y → k' = k0) Hk0pack).
We use k0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (ordsuccI1 m1 k0 Hk0In).
We prove the intermediate claim Hk0Dom: k0 ∈ ordsucc m1.
An exact proof term for the current goal is (ordsuccI1 m1 k0 Hk0In).
rewrite the current goal using (apply_fun_graph (ordsucc m1) (λk : set ⇒ If_i (k = m1) lastval (apply_fun e1 k)) k0 Hk0Dom) (from left to right).
We prove the intermediate claim Hk0nm1: ¬ (k0 = m1).
Assume Heq: k0 = m1.
We prove the intermediate claim Hmm1: m1 ∈ m1.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hk0In.
An exact proof term for the current goal is ((In_irref m1) Hmm1).
rewrite the current goal using (If_i_0 (k0 = m1) lastval (apply_fun e1 k0) Hk0nm1) (from left to right).
An exact proof term for the current goal is Hk0Eq.
Let k' be given.
Assume Hk'Dom: k' ∈ ordsucc m1.
Assume Heq: apply_fun e2 k' = y.
Apply (xm (k' = m1)) to the current goal.
Assume Hkm1: k' = m1.
Apply FalseE to the current goal.
We prove the intermediate claim He2kLast: apply_fun e2 k' = lastval.
We will prove apply_fun e2 k' = lastval.
rewrite the current goal using Hkm1 (from left to right).
An exact proof term for the current goal is He2m1.
We prove the intermediate claim HyEqA: y = apply_fun e2 k'.
rewrite the current goal using Heq (from right to left).
Use reflexivity.
We prove the intermediate claim HyEqLast: y = lastval.
An exact proof term for the current goal is (eq_i_tra y (apply_fun e2 k') lastval HyEqA He2kLast).
An exact proof term for the current goal is (HyNLast HyEqLast).
Assume Hkn: ¬ (k' = m1).
We prove the intermediate claim HkInM1: k' ∈ m1.
Apply (ordsuccE m1 k' Hk'Dom) to the current goal.
Assume HkM1: k' ∈ m1.
An exact proof term for the current goal is HkM1.
Assume Hkeq: k' = m1.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hkn Hkeq).
We prove the intermediate claim He2k: apply_fun e2 k' = apply_fun e1 k'.
rewrite the current goal using (apply_fun_graph (ordsucc m1) (λk0 : set ⇒ If_i (k0 = m1) lastval (apply_fun e1 k0)) k' Hk'Dom) (from left to right).
rewrite the current goal using (If_i_0 (k' = m1) lastval (apply_fun e1 k') Hkn) (from left to right).
Use reflexivity.
We prove the intermediate claim He1eqY: apply_fun e1 k' = y.
We will prove apply_fun e1 k' = y.
rewrite the current goal using He2k (from right to left).
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (Hk0uniq k' HkInM1 He1eqY).
We prove the intermediate claim HtermLastUI: apply_fun lastval x ∈ unit_interval.
An exact proof term for the current goal is (HvalUI0 lastval HlastF0).
We prove the intermediate claim HsumFull: nat_primrec 0 (step e0) (ordsucc m1) = nat_primrec 0 (step e2) (ordsucc m1).
rewrite the current goal using (nat_primrec_S 0 (step e0) m1 Hm1Nat) (from left to right).
rewrite the current goal using (nat_primrec_S 0 (step e2) m1 Hm1Nat) (from left to right).
We prove the intermediate claim HaccEq: nat_primrec 0 (step e0) m1 = nat_primrec 0 (step e2) m1.
We prove the intermediate claim Hacc1: nat_primrec 0 (step e0) m1 = nat_primrec 0 (step e1) m1.
rewrite the current goal using Hm1Def (from left to right).
An exact proof term for the current goal is HsumSmall.
We prove the intermediate claim Hacc2: nat_primrec 0 (step e1) m1 = nat_primrec 0 (step e2) m1.
We prove the intermediate claim HeqE1E2: ∀k : set, k ∈ m1 → apply_fun e1 k = apply_fun e2 k.
Let k be given.
Assume HkM1: k ∈ m1.
We prove the intermediate claim HkDom: k ∈ ordsucc m1.
An exact proof term for the current goal is (ordsuccI1 m1 k HkM1).
We prove the intermediate claim Hknm1: ¬ (k = m1).
Assume Heq: k = m1.
We prove the intermediate claim Hmm1: m1 ∈ m1.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is HkM1.
An exact proof term for the current goal is ((In_irref m1) Hmm1).
We prove the intermediate claim He2k: apply_fun e2 k = apply_fun e1 k.
rewrite the current goal using (apply_fun_graph (ordsucc m1) (λk0 : set ⇒ If_i (k0 = m1) lastval (apply_fun e1 k0)) k HkDom) (from left to right).
rewrite the current goal using (If_i_0 (k = m1) lastval (apply_fun e1 k) Hknm1) (from left to right).
Use reflexivity.
We will prove apply_fun e1 k = apply_fun e2 k.
rewrite the current goal using He2k (from right to left).
Use reflexivity.
An exact proof term for the current goal is (nat_primrec_sum_congr_on X m1 e1 e2 x Hm1Nat HxX HeqE1E2).
An exact proof term for the current goal is (eq_i_tra (nat_primrec 0 (step e0) m1) (nat_primrec 0 (step e1) m1) (nat_primrec 0 (step e2) m1) Hacc1 Hacc2).
rewrite the current goal using HaccEq (from left to right).
We prove the intermediate claim He2m1F: apply_fun e2 m1 = lastval.
An exact proof term for the current goal is He2m1.
rewrite the current goal using He2m1F (from left to right).
Use reflexivity.
Set e' to be the term swap_adjacent e2 t (ordsucc m1).
We use e' to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HtIn: t ∈ ordsucc m1.
An exact proof term for the current goal is (ordsuccI1 m1 t (ordsuccI2 t)).
We prove the intermediate claim HstIn: ordsucc t ∈ ordsucc m1.
rewrite the current goal using Hm1Def (from right to left).
An exact proof term for the current goal is (ordsuccI2 m1).
An exact proof term for the current goal is (bijection_swap_adjacent F0 e2 t (ordsucc m1) HtIn HstIn Hbij2).
We prove the intermediate claim HtermUI2: ∀k : set, k ∈ ordsucc m1 → apply_fun (apply_fun e2 k) x ∈ unit_interval.
Let k be given.
Assume HkDom: k ∈ ordsucc m1.
Apply (xm (k = m1)) to the current goal.
Assume Hkm1: k = m1.
rewrite the current goal using Hkm1 (from left to right).
rewrite the current goal using He2m1 (from left to right).
An exact proof term for the current goal is HtermLastUI.
Assume Hknm1: ¬ (k = m1).
We prove the intermediate claim HkInM1: k ∈ m1.
Apply (ordsuccE m1 k HkDom) to the current goal.
Assume HkM1: k ∈ m1.
An exact proof term for the current goal is HkM1.
Assume Hkeq: k = m1.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hknm1 Hkeq).
We prove the intermediate claim He1fun: function_on e1 m1 (F0 ∖ {lastval}).
An exact proof term for the current goal is (andEL (function_on e1 m1 (F0 ∖ {lastval})) (∀y0 : set, y0 ∈ (F0 ∖ {lastval}) → ∃x0 : set, x0 ∈ m1 ∧ apply_fun e1 x0 = y0 ∧ (∀x' : set, x' ∈ m1 → apply_fun e1 x' = y0 → x' = x0)) Hbij1).
We prove the intermediate claim He1kDrop: apply_fun e1 k ∈ (F0 ∖ {lastval}).
An exact proof term for the current goal is (He1fun k HkInM1).
We prove the intermediate claim He2k: apply_fun e2 k = apply_fun e1 k.
rewrite the current goal using (apply_fun_graph (ordsucc m1) (λk0 : set ⇒ If_i (k0 = m1) lastval (apply_fun e1 k0)) k HkDom) (from left to right).
rewrite the current goal using (If_i_0 (k = m1) lastval (apply_fun e1 k) Hknm1) (from left to right).
Use reflexivity.
rewrite the current goal using He2k (from left to right).
An exact proof term for the current goal is (HvalUI0 (apply_fun e1 k) (setminusE1 F0 {lastval} (apply_fun e1 k) He1kDrop)).
We prove the intermediate claim HswapEq: nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun (swap_adjacent e2 t (ordsucc m1)) k) x)) (ordsucc m1) = nat_primrec 0 (step e2) (ordsucc m1).
We prove the intermediate claim HnO: ordsucc m1 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc m1 Hm1O2).
We prove the intermediate claim HtInM1: t ∈ m1.
rewrite the current goal using Hm1Def (from left to right).
An exact proof term for the current goal is (ordsuccI2 t).
We prove the intermediate claim HtIn: t ∈ ordsucc m1.
An exact proof term for the current goal is (ordsuccI1 m1 t HtInM1).
We prove the intermediate claim HstIn: ordsucc t ∈ ordsucc m1.
rewrite the current goal using Hm1Def (from right to left) at position 1.
An exact proof term for the current goal is (ordsuccI2 m1).
An exact proof term for the current goal is (nat_primrec_sum_swap_adjacent_unit_interval X (ordsucc m1) e2 t x HnO HtIn HstIn HxX HtermUI2).
We prove the intermediate claim HswapRev: nat_primrec 0 (step e2) (ordsucc m1) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun (swap_adjacent e2 t (ordsucc m1)) k) x)) (ordsucc m1).
rewrite the current goal using HswapEq (from left to right).
Use reflexivity.
An exact proof term for the current goal is (eq_i_tra (nat_primrec 0 (step e0) (ordsucc m1)) (nat_primrec 0 (step e2) (ordsucc m1)) (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun (swap_adjacent e2 t (ordsucc m1)) k) x)) (ordsucc m1)) HsumFull HswapRev).
We prove the intermediate claim HappLast: apply_fun e' m1 = apply_fun e2 t.
We prove the intermediate claim Hm1Dom: m1 ∈ ordsucc m1.
An exact proof term for the current goal is (ordsuccI2 m1).
rewrite the current goal using Hm1Def (from left to right) at position 1.
We prove the intermediate claim Hsa: apply_fun (swap_adjacent e2 t (ordsucc m1)) (ordsucc t) = apply_fun e2 t.
An exact proof term for the current goal is (swap_adjacent_at_succ e2 t (ordsucc m1) (ordsuccI2 m1)).
An exact proof term for the current goal is Hsa.
rewrite the current goal using HappLast (from left to right).
We prove the intermediate claim HtDom: t ∈ ordsucc m1.
An exact proof term for the current goal is (ordsuccI1 m1 t (ordsuccI2 t)).
We prove the intermediate claim HtNeM1: ¬ (t = m1).
Assume Heq: t = m1.
We prove the intermediate claim Hm1m1: m1 ∈ m1.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is (ordsuccI2 t).
An exact proof term for the current goal is ((In_irref m1) Hm1m1).
We prove the intermediate claim He2t: apply_fun e2 t = apply_fun e1 t.
rewrite the current goal using (apply_fun_graph (ordsucc m1) (λk0 : set ⇒ If_i (k0 = m1) lastval (apply_fun e1 k0)) t HtDom) (from left to right).
rewrite the current goal using (If_i_0 (t = m1) lastval (apply_fun e1 t) HtNeM1) (from left to right).
Use reflexivity.
rewrite the current goal using He2t (from left to right).
An exact proof term for the current goal is He1last.
We prove the intermediate claim HPm: Pm m.
An exact proof term for the current goal is (nat_ind Pm HP0 HPS m HmNat).
An exact proof term for the current goal is (HPm F e flast HmO Hbij HflF HvalUI).
∎