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

Question

Это утверждение кажется мне очевидным, если только я не пропущу какой-то контрпример, но я не смог найти ничего в библиотеке списков Coq, которая бы это делала. Есть ли команда, которая что-то делает для этого?

Answer 1

Обычно это можно получить с помощью тактики injection. Вариант леммы для переписывания можно найти в math-comp:

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