Let X and Y be given.

Assume H1: Inj1 X = Inj1 Y.

We will prove X = Y.

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

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

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

Use reflexivity.

∎