小编Fel*_*lbi的帖子

有人可以解释一下如何完成这个证明吗？（请不要给出实际答案，只是一些指导:)

练习来自 SF 第 1 卷，如标题所示，内容如下：

(** **** 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.

现在，我在介绍所有术语后尝试通过injectionon来解决这个问题H0。injection经过重写后H2，我最终得到了以下目标，但我不知道如何前进。

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