Let z be given.

Assume H1: z ∈ 0 + X.

We will prove z ∈ Inj0 X.

Apply (setsum_Inj_inv 0 X z H1) to the current goal.

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

Apply (exandE_i (λx ⇒ x ∈ 0) (λx ⇒ z = Inj0 x) H2) to the current goal.

Let x be given.

Assume H3: x ∈ 0.

We will prove False.

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

Assume H2: ∃x ∈ X, z = Inj1 x.

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ z = Inj1 x) H2) to the current goal.

Let x be given.

Assume H3: x ∈ X.

Assume H4: z = Inj1 x.

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

We will prove Inj1 x ∈ Inj0 X.

An exact proof term for the current goal is (Inj0I X x H3).

Let z be given.

Assume H1: z ∈ Inj0 X.

We will prove z ∈ 0 + X.

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ z = Inj1 x) (Inj0E X z H1)) to the current goal.

Let x be given.

Assume H2: x ∈ X.

Assume H3: z = Inj1 x.

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

We will prove Inj1 x ∈ 0 + X.

Apply Inj1_setsum to the current goal.

An exact proof term for the current goal is H2.