We use (λx : set ⇒ (x,minus_SNo x)) to witness the existential quantifier.

Apply (injI Sorgenfrey_line Sorgenfrey_plane_L (λx : set ⇒ (x,minus_SNo x))) to the current goal.

Let x be given.

An exact proof term for the current goal is (ReplI Sorgenfrey_line (λx0 : set ⇒ (x0,minus_SNo x0)) x HxR).

Let x1 be given.

Assume Hx1: x1 ∈ Sorgenfrey_line.

Let x2 be given.

Assume Hx2: x2 ∈ Sorgenfrey_line.

Assume Heq: (x1,minus_SNo x1) = (x2,minus_SNo x2).

We will prove x1 = x2.

We prove the intermediate claim H0: (x1,minus_SNo x1) 0 = (x2,minus_SNo x2) 0.

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

Use reflexivity.

We prove the intermediate claim Hx10: (x1,minus_SNo x1) 0 = x1.

rewrite the current goal using (tuple_pair x1 (minus_SNo x1)) (from right to left).

An exact proof term for the current goal is (pair_ap_0 x1 (minus_SNo x1)).

We prove the intermediate claim Hx20: (x2,minus_SNo x2) 0 = x2.

rewrite the current goal using (tuple_pair x2 (minus_SNo x2)) (from right to left).

An exact proof term for the current goal is (pair_ap_0 x2 (minus_SNo x2)).

rewrite the current goal using Hx10 (from right to left) at position 1.

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

An exact proof term for the current goal is H0.