We prove the intermediate claim Hdef: ex50_R3_e3 = graph 3 (λi : set ⇒ if i = 2 then 1 else 0).

Use reflexivity.

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

Apply (graph3_in_euclidean_space3 (λi : set ⇒ if i = 2 then 1 else 0)) to the current goal.

Let i be given.

We prove the intermediate claim Happ: (λi0 : set ⇒ if i0 = 2 then 1 else 0) i = (if i = 2 then 1 else 0).

Use reflexivity.

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

Apply (xm (i = 2)) to the current goal.

Assume Hi2: i = 2.

We prove the intermediate claim Hif: (if i = 2 then 1 else 0) = 1.

An exact proof term for the current goal is (If_i_1 (i = 2) 1 0 Hi2).

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

An exact proof term for the current goal is real_1.

Assume Hni2: ¬ (i = 2).

We prove the intermediate claim Hif: (if i = 2 then 1 else 0) = 0.

An exact proof term for the current goal is (If_i_0 (i = 2) 1 0 Hni2).

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

An exact proof term for the current goal is real_0.

∎