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

An exact proof term for the current goal is Inj1_setsum.

∎