Let n, f and g be given.
Assume HnO: n ∈ ω.
Assume Hf: f ∈ euclidean_space n.
Assume Hg: g ∈ euclidean_space n.
Assume Hext: euclidean_space_extend_to_Romega n f = euclidean_space_extend_to_Romega n g.
Apply xm (f = g) to the current goal.
Assume Heq.
An exact proof term for the current goal is Heq.
Assume Hneq: ¬ (f = g).
We prove the intermediate claim Hex: ∃i : set, i ∈ n ∧ apply_fun f i ≠ apply_fun g i.
An exact proof term for the current goal is (product_space_points_differ_coord n (const_space_family n R R_standard_topology) f g Hf Hg Hneq).
Apply FalseE to the current goal.
Apply Hex to the current goal.
Let i be given.
Assume Hipair.
We prove the intermediate claim Hin: i ∈ n.
An exact proof term for the current goal is (andEL (i ∈ n) (apply_fun f i ≠ apply_fun g i) Hipair).
We prove the intermediate claim Hdiff: apply_fun f i ≠ apply_fun g i.
An exact proof term for the current goal is (andER (i ∈ n) (apply_fun f i ≠ apply_fun g i) Hipair).
We prove the intermediate claim HnSub: n ⊆ ω.
An exact proof term for the current goal is (omega_TransSet n HnO).
We prove the intermediate claim HiO: i ∈ ω.
An exact proof term for the current goal is (HnSub i Hin).
Set ef to be the term euclidean_space_extend_to_Romega n f.
Set eg to be the term euclidean_space_extend_to_Romega n g.
We prove the intermediate claim HappEq: apply_fun ef i = apply_fun eg i.
rewrite the current goal using Hext (from left to right).
Use reflexivity.
We prove the intermediate claim Hapf: apply_fun ef i = If_i (i ∈ n) (apply_fun f i) 0.
An exact proof term for the current goal is (euclidean_space_extend_to_Romega_apply n f i HiO).
We prove the intermediate claim Hapg: apply_fun eg i = If_i (i ∈ n) (apply_fun g i) 0.
An exact proof term for the current goal is (euclidean_space_extend_to_Romega_apply n g i HiO).
We prove the intermediate claim Hapf': apply_fun ef i = apply_fun f i.
rewrite the current goal using Hapf (from left to right).
rewrite the current goal using (If_i_1 (i ∈ n) (apply_fun f i) 0 Hin) (from left to right).
Use reflexivity.
We prove the intermediate claim Hapg': apply_fun eg i = apply_fun g i.
rewrite the current goal using Hapg (from left to right).
rewrite the current goal using (If_i_1 (i ∈ n) (apply_fun g i) 0 Hin) (from left to right).
Use reflexivity.
We prove the intermediate claim Heqfg: apply_fun f i = apply_fun g i.
rewrite the current goal using Hapf' (from right to left).
rewrite the current goal using Hapg' (from right to left).
An exact proof term for the current goal is HappEq.
An exact proof term for the current goal is (Hdiff Heqfg).
∎