coq - 软件基础第 1 卷：策略：injection_ex3

Question

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

该练习来自 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.

现在，我试图在介绍完所有术语后解决这个injection问题。H0在injection重写之后H2，我最终达到了以下目标，我不知道如何前进。

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

很明显，如果我设法添加:: l到等式的两边，那么我可以完成reflexivity，但是什么策略可以让我添加:: l到两边？

此致

Answer 1

从H3和H1，您应该能够得到一个假设，您可以再次使用注入来得出结论。