Software Foundations Volume 1: Tactics: injection_ex3

Question

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 (injection_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

Answer 1

From H3 and H1, you should be able to get a hypothesis on which you can use injection again to conclude.