Let X, n, e1, e2 and x be given.
Assume HnNat: nat_p n.
Assume HxX: x ∈ X.
Assume Heq: ∀k : set, k ∈ n → apply_fun e1 k = apply_fun e2 k.
Set step1 to be the term (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e1 k) x)).
Set step2 to be the term (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)).
Set Psum to be the term (λm : set ⇒ ∀ea eb : set, (∀k : set, k ∈ m → apply_fun ea k = apply_fun eb k) → nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun ea k) x)) m = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb k) x)) m).
We prove the intermediate claim HP0: Psum 0.
Let ea and eb be given.
Assume Heq0: ∀k : set, k ∈ 0 → apply_fun ea k = apply_fun eb k.
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).
Use reflexivity.
We prove the intermediate claim HPS: ∀m : set, nat_p m → Psum m → Psum (ordsucc m).
Let m be given.
Assume HmNat: nat_p m.
Assume IHm: Psum m.
We will prove Psum (ordsucc m).
Let ea and eb be given.
Assume HeqS: ∀k : set, k ∈ ordsucc m → apply_fun ea k = apply_fun eb k.
rewrite the current goal using (nat_primrec_S 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun ea k) x)) m HmNat) (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)) m HmNat) (from left to right).
We prove the intermediate claim Heqm: ∀k : set, k ∈ m → apply_fun ea k = apply_fun eb k.
Let k be given.
Assume HkM: k ∈ m.
An exact proof term for the current goal is (HeqS k (ordsuccI1 m k HkM)).
We prove the intermediate claim Hacc: nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun ea k) x)) m = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun eb k) x)) m.
An exact proof term for the current goal is (IHm ea eb Heqm).
We prove the intermediate claim Hem: apply_fun ea m = apply_fun eb m.
An exact proof term for the current goal is (HeqS m (ordsuccI2 m)).
rewrite the current goal using Hacc (from left to right) at position 1.
rewrite the current goal using Hem (from left to right).
Use reflexivity.
We prove the intermediate claim HPn: Psum n.
An exact proof term for the current goal is (nat_ind Psum HP0 HPS n HnNat).
We prove the intermediate claim HnIn: n ∈ ordsucc n.
An exact proof term for the current goal is (ordsuccI2 n).
We prove the intermediate claim Hstep1: nat_primrec 0 step1 n = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e1 k) x)) n.
Use reflexivity.
We prove the intermediate claim Hstep2: nat_primrec 0 step2 n = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) n.
Use reflexivity.
rewrite the current goal using Hstep1 (from right to left).
rewrite the current goal using Hstep2 (from right to left).
An exact proof term for the current goal is (HPn e1 e2 Heq).
∎