Coq: (a :: L1) = (b :: L2) ⇒ a = b ∧ L1 = L2?

Question

这句话对我来说似乎很明显，除非我忽略了一些反例，但我在Coq列表库中找不到任何能做到这一点的东西。有没有这样的命令？

Answer 1

这通常可以使用injection策略导出。重写引理的一个版本可以在数学组件中找到：

eqseq_cons (T : eqType) (x1 x2 : T) (s1 s2 : seq T) :
(x1 :: s1 == x2 :: s2) = (x1 == x2) && (s1 == s2).