Let x be given.
Assume HxX: x ∈ setprod 2 ω.
Assume Hneq10: x ≠ (1,0).
Apply (Sigma_E 2 (λ_ : set ⇒ ω) x HxX) to the current goal.
Let i be given.
Assume HiPair.
Apply HiPair to the current goal.
Assume Hi2 HmPair.
Apply HmPair to the current goal.
Let m be given.
Assume HmPair2.
Apply HmPair2 to the current goal.
Assume HmO HxEqPair.
We prove the intermediate claim HxEq: x = (i,m).
rewrite the current goal using HxEqPair (from left to right).
An exact proof term for the current goal is (tuple_pair i m).
We prove the intermediate claim Hi01: i ∈ {0,1}.
An exact proof term for the current goal is (Subq_2_UPair01 i Hi2).
Apply (UPairE i 0 1 Hi01 ({x} ∈ order_topology (setprod 2 ω))) to the current goal.
Assume Hi0: i = 0.
rewrite the current goal using HxEq (from left to right).
rewrite the current goal using Hi0 (from left to right).
An exact proof term for the current goal is (singleton_setprod_2_omega_0k_open m HmO).
Assume Hi1: i = 1.
Apply (xm (m = 0)) to the current goal.
Assume Hm0: m = 0.
Apply FalseE to the current goal.
Apply Hneq10 to the current goal.
rewrite the current goal using HxEq (from left to right).
rewrite the current goal using Hi1 (from left to right).
rewrite the current goal using Hm0 (from left to right).
Use reflexivity.
Assume Hmneq0: ¬ (m = 0).
rewrite the current goal using HxEq (from left to right).
rewrite the current goal using Hi1 (from left to right).
An exact proof term for the current goal is (singleton_setprod_2_omega_1n_open_if_nonzero m HmO Hmneq0).
∎