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

Let i be given.

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

Use reflexivity.

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

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

Assume Hi0: i = 0.

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

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

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

An exact proof term for the current goal is real_1.

Assume Hni0: ¬ (i = 0).

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

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

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

An exact proof term for the current goal is real_0.

∎