We prove the intermediate claim Hdef: ex50_R3_e2 = graph 3 (λi : set ⇒ if i = 1 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 = 1 then 1 else 0)) to the current goal.

Let i be given.

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

Use reflexivity.

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

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

Assume Hi1: i = 1.

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

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

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

An exact proof term for the current goal is real_1.

Assume Hni1: ¬ (i = 1).

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

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

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

An exact proof term for the current goal is real_0.

∎