Let y be given.

Assume Hy: y ∈ Inj1 0.

We will prove y ∈ 1.

We prove the intermediate claim Hcase: y = 0 ∨ ∃x ∈ 0, y = Inj1 x.

An exact proof term for the current goal is (Inj1E 0 y Hy).

Apply (Hcase (y ∈ 1)) to the current goal.

Assume Hy0: y = 0.

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

An exact proof term for the current goal is In_0_1.

Assume Hex: ∃x ∈ 0, y = Inj1 x.

Apply Hex to the current goal.

Let x be given.

Assume Hxp.

Apply Hxp to the current goal.

Assume Hx0 HyEq.

Apply FalseE to the current goal.

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

Let y be given.

Assume Hy: y ∈ 1.

We will prove y ∈ Inj1 0.

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 Hy.

We prove the intermediate claim Hy0: y = 0.

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

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

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