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
From H3 and H1, you should be able to get a hypothesis on which you can use injection again to conclude.