Let x be given.

Assume H1: Inj1 x ∈ {0}.

An exact proof term for the current goal is (Inj1NE1 x (SingE 0 (Inj1 x) H1)).

∎