Let z be given.

Assume Hz: z ∈ (0,1).

We will prove z ∈ {1}.

We prove the intermediate claim Hzsum: z ∈ 0 + 1.

We will prove z ∈ 0 + 1.

rewrite the current goal using (tuple_pair 0 1) (from left to right).

An exact proof term for the current goal is Hz.

We prove the intermediate claim Hcases: (∃x ∈ 0, z = Inj0 x) ∨ (∃y ∈ 1, z = Inj1 y).

An exact proof term for the current goal is (setsum_Inj_inv 0 1 z Hzsum).

Apply (Hcases (z ∈ {1})) to the current goal.

Assume Hex: ∃x ∈ 0, z = Inj0 x.

Apply Hex to the current goal.

Let x be given.

Assume Hxp.

Apply Hxp to the current goal.

Assume Hx0 HzEq.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE x Hx0).

Assume Hex: ∃y ∈ 1, z = Inj1 y.

Apply Hex to the current goal.

Let y be given.

Assume Hyp.

Apply Hyp to the current goal.

Assume Hy1 HzEq.

We prove the intermediate claim HySing: y ∈ {0}.

We will prove y ∈ {0}.

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

An exact proof term for the current goal is Hy1.

We prove the intermediate claim Hy0: y = 0.

An exact proof term for the current goal is (SingE 0 y HySing).

We prove the intermediate claim HzInj10: z = Inj1 0.

We will prove z = Inj1 0.

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

An exact proof term for the current goal is HzEq.

We prove the intermediate claim Hz1: z = 1.

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

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

Use reflexivity.

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

An exact proof term for the current goal is (SingI 1).

Let z be given.

Assume Hz: z ∈ {1}.

We will prove z ∈ (0,1).

rewrite the current goal using (tuple_pair 0 1) (from right to left).

We prove the intermediate claim Hz1: z = 1.

An exact proof term for the current goal is (SingE 1 z Hz).

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

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

An exact proof term for the current goal is (Inj1_setsum 0 1 0 In_0_1).