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

We will prove Inj0 0 = 0.

An exact proof term for the current goal is Inj0_0.

∎