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

An exact proof term for the current goal is Inj0_setsum.

∎