Let X and Y be given.

Assume H1: Inj0 X = Inj0 Y.

We will prove X = Y.

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

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

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

Use reflexivity.

∎