Assume Hnot: ¬ (∃n : set, n ∈ ω ∧ apply_fun f n ≠ apply_fun g n).

We prove the intermediate claim Heqpt: ∀n : set, n ∈ ω → apply_fun f n = apply_fun g n.

Let n be given.

Assume Hn: n ∈ ω.

Apply (xm (apply_fun f n = apply_fun g n) (apply_fun f n = apply_fun g n)) to the current goal.

Assume Heq.

An exact proof term for the current goal is Heq.

Assume Hneqval: ¬ (apply_fun f n = apply_fun g n).

We prove the intermediate claim Hex: ∃k : set, k ∈ ω ∧ apply_fun f k ≠ apply_fun g k.

We use n to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hn.

Assume Heq.

An exact proof term for the current goal is (Hneqval Heq).

An exact proof term for the current goal is (FalseE (Hnot Hex) (apply_fun f n = apply_fun g n)).

We prove the intermediate claim Hpowf: f ∈ 𝒫 (setprod ω R).

An exact proof term for the current goal is (real_sequences_in_Power_setprod f Hf).

We prove the intermediate claim Hpowg: g ∈ 𝒫 (setprod ω R).

An exact proof term for the current goal is (real_sequences_in_Power_setprod g Hg).

We prove the intermediate claim Hsubf: f ⊆ setprod ω R.

An exact proof term for the current goal is (PowerE (setprod ω R) f Hpowf).

We prove the intermediate claim Hsubg: g ⊆ setprod ω R.

An exact proof term for the current goal is (PowerE (setprod ω R) g Hpowg).

We prove the intermediate claim Htotf: total_function_on f ω R.

An exact proof term for the current goal is (real_sequences_total f Hf).

We prove the intermediate claim Htotg: total_function_on g ω R.

An exact proof term for the current goal is (real_sequences_total g Hg).

We prove the intermediate claim Hfunf: functional_graph f.

An exact proof term for the current goal is (real_sequences_functional f Hf).

We prove the intermediate claim Hfung: functional_graph g.

An exact proof term for the current goal is (real_sequences_functional g Hg).

We prove the intermediate claim Hsub_fg: f ⊆ g.

Let p be given.

Assume Hp: p ∈ f.

We will prove p ∈ g.

We prove the intermediate claim HpProd: p ∈ setprod ω R.

An exact proof term for the current goal is (Hsubf p Hp).

Apply (Sigma_E ω (λ_ : set ⇒ R) p HpProd) to the current goal.

Let n be given.

Assume Hn_pair.

Apply Hn_pair to the current goal.

Assume Hn: n ∈ ω.

Assume Hrest.

Apply Hrest to the current goal.

Let y be given.

Assume Hy_pair.

Apply Hy_pair to the current goal.

Assume Hy: y ∈ R.

Assume Hpdef.

We prove the intermediate claim HpdefT: p = (n,y).

rewrite the current goal using (tuple_pair n y) (from right to left) at position 1.

An exact proof term for the current goal is Hpdef.

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

We prove the intermediate claim Hpf: (n,y) ∈ f.

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

An exact proof term for the current goal is Hp.

We prove the intermediate claim Happf: apply_fun f n = y.

An exact proof term for the current goal is (functional_graph_apply_fun_eq f n y Hfunf Hpf).

We prove the intermediate claim Happg: apply_fun g n = y.

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

Use symmetry.

An exact proof term for the current goal is (Heqpt n Hn).

We prove the intermediate claim Hpg: (n,apply_fun g n) ∈ g.

An exact proof term for the current goal is (total_function_on_apply_fun_in_graph g ω R n Htotg Hn).

We prove the intermediate claim HtupEq: (n,apply_fun g n) = (n,y).

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

Use reflexivity.

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

An exact proof term for the current goal is Hpg.

We prove the intermediate claim Hsub_gf: g ⊆ f.

Let p be given.

Assume Hp: p ∈ g.

We will prove p ∈ f.

We prove the intermediate claim HpProd: p ∈ setprod ω R.

An exact proof term for the current goal is (Hsubg p Hp).

Apply (Sigma_E ω (λ_ : set ⇒ R) p HpProd) to the current goal.

Let n be given.

Assume Hn_pair.

Apply Hn_pair to the current goal.

Assume Hn: n ∈ ω.

Assume Hrest.

Apply Hrest to the current goal.

Let y be given.

Assume Hy_pair.

Apply Hy_pair to the current goal.

Assume Hy: y ∈ R.

Assume Hpdef.

We prove the intermediate claim HpdefT: p = (n,y).

rewrite the current goal using (tuple_pair n y) (from right to left) at position 1.

An exact proof term for the current goal is Hpdef.

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

We prove the intermediate claim Hpg: (n,y) ∈ g.

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

An exact proof term for the current goal is Hp.

We prove the intermediate claim Happg: apply_fun g n = y.

An exact proof term for the current goal is (functional_graph_apply_fun_eq g n y Hfung Hpg).

We prove the intermediate claim Happf: apply_fun f n = y.

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

An exact proof term for the current goal is (Heqpt n Hn).

We prove the intermediate claim Hpf: (n,apply_fun f n) ∈ f.

An exact proof term for the current goal is (total_function_on_apply_fun_in_graph f ω R n Htotf Hn).

We prove the intermediate claim HtupEq: (n,apply_fun f n) = (n,y).

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

Use reflexivity.

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

An exact proof term for the current goal is Hpf.

We prove the intermediate claim Heq: f = g.

An exact proof term for the current goal is (set_ext f g Hsub_fg Hsub_gf).

An exact proof term for the current goal is (FalseE (Hneq Heq) (∃n : set, n ∈ ω ∧ apply_fun f n ≠ apply_fun g n)).