Let X and Y be given.

Assume H1: Inj0 X = Inj1 Y.

We prove the intermediate claim L1: 0 ∈ Inj1 Y.

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

We prove the intermediate claim L2: 0 ∈ Inj0 X.

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

An exact proof term for the current goal is L1.

Apply (Inj0E X 0 L2) to the current goal.

Let x be given.

Assume H2: x ∈ X ∧ 0 = Inj1 x.

Apply Inj1NE1 x to the current goal.

Use symmetry.

An exact proof term for the current goal is andER (x ∈ X) (0 = Inj1 x) H2.

∎