Let x be given.

Assume H1: Inj1 x = 0.

Apply (EmptyE 0) to the current goal.

We will prove 0 ∈ 0.

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

We will prove 0 ∈ Inj1 x.

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

∎