Let n be given.
Assume Hn: n ∈ ω.
We will prove apply_fun seq_one_over_n n = inv_nat (ordsucc n).
Set f to be the term seq_one_over_n.
We prove the intermediate claim HinvIn: inv_nat (ordsucc n) ∈ {inv_nat (ordsucc n)}.
An exact proof term for the current goal is (SingI (inv_nat (ordsucc n))).
We prove the intermediate claim HpairIn: (n,inv_nat (ordsucc n)) ∈ f.
An exact proof term for the current goal is (lamI2 ω (λk : set ⇒ {inv_nat (ordsucc k)}) n Hn (inv_nat (ordsucc n)) HinvIn).
We prove the intermediate claim Happair: (n,apply_fun f n) ∈ f.
An exact proof term for the current goal is (Eps_i_ax (λy : set ⇒ (n,y) ∈ f) (inv_nat (ordsucc n)) HpairIn).
Apply (lamE ω (λk : set ⇒ {inv_nat (ordsucc k)}) (n,apply_fun f n) Happair) to the current goal.
Let x0 be given.
Assume Hx0_conj.
Apply Hx0_conj to the current goal.
Assume Hx0 Hexy0.
Apply Hexy0 to the current goal.
Let y0 be given.
Assume Hy0_conj.
Apply Hy0_conj to the current goal.
Assume Hy0 Heq.
We prove the intermediate claim HeqT: (n,apply_fun f n) = (x0,y0).
rewrite the current goal using (tuple_pair x0 y0) (from right to left).
An exact proof term for the current goal is Heq.
We prove the intermediate claim H0eq: (n,apply_fun f n) 0 = (x0,y0) 0.
rewrite the current goal using HeqT (from left to right).
Use reflexivity.
We prove the intermediate claim H1eq: (n,apply_fun f n) 1 = (x0,y0) 1.
rewrite the current goal using HeqT (from left to right).
Use reflexivity.
We prove the intermediate claim Hnx0: n = x0.
We will prove n = x0.
rewrite the current goal using (tuple_2_0_eq n (apply_fun f n)) (from right to left).
rewrite the current goal using (tuple_2_0_eq x0 y0) (from right to left).
An exact proof term for the current goal is H0eq.
We prove the intermediate claim Happ: apply_fun f n = y0.
We will prove apply_fun f n = y0.
rewrite the current goal using (tuple_2_1_eq n (apply_fun f n)) (from right to left).
rewrite the current goal using (tuple_2_1_eq x0 y0) (from right to left).
An exact proof term for the current goal is H1eq.
We prove the intermediate claim Hy0eq: y0 = inv_nat (ordsucc x0).
An exact proof term for the current goal is (SingE (inv_nat (ordsucc x0)) y0 Hy0).
We prove the intermediate claim Hx0n: x0 = n.
rewrite the current goal using Hnx0 (from left to right).
Use reflexivity.
rewrite the current goal using Happ (from left to right).
rewrite the current goal using Hy0eq (from left to right).
rewrite the current goal using Hx0n (from left to right).
Use reflexivity.
∎