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

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

An exact proof term for the current goal is setsum_Inj_inv.

∎