Could some explain how to complete this proof? (please don't give the actual answer, just some guidance :)

The exercise is from SF volume1, as stated in the title and it goes like this:

```
(** **** Exercise: 3 stars, standard (ex3) *)
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ->
j = z :: l ->
x = y.
```

Now, I'm trying to tackle this by `injection`

on `H0`

after introducing all terms. After `injection`

and rewriting by `H2`

, I end up with the following goal and I have no idea how to move forward.

```
1 subgoal (ID 174)
X : Type
x, y, z : X
l, j : list X
H2 : x = z
H3 : y :: l = j
H1 : j = z :: l
============================
z = y
```

It's clear that if I manage to add `:: l`

to both sides of the equation, then I can complete with `reflexivity`

, but what tactic would allow me to add `:: l`

to both sides?

Best regards