Let z be given.

Assume H1: z ∈ 1 + X.

We will prove z ∈ Inj1 X.

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

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

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

Let x be given.

Assume H3: x ∈ 1.

Assume H4: z = Inj0 x.

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

We will prove Inj0 x ∈ Inj1 X.

We prove the intermediate claim L1: x = 0.

An exact proof term for the current goal is (SingE 0 x (Subq_1_Sing0 x H3)).

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

We will prove Inj0 0 ∈ Inj1 X.

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

We will prove 0 ∈ Inj1 X.

An exact proof term for the current goal is (Inj1I1 X).

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 ∈ Inj1 X.

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

Let z be given.

Assume H1: z ∈ Inj1 X.

We will prove z ∈ 1 + X.

Apply (Inj1E X z H1) to the current goal.

Assume H2: z = 0.

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

We will prove 0 ∈ 1 + X.

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

We will prove Inj0 0 ∈ 1 + X.

Apply Inj0_setsum to the current goal.

We will prove 0 ∈ 1.

An exact proof term for the current goal is In_0_1.

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 H2: x ∈ X.

Assume H3: z = Inj1 x.

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

We will prove Inj1 x ∈ 1 + X.

Apply Inj1_setsum to the current goal.

An exact proof term for the current goal is H2.