diff options
Diffstat (limited to 'theories/Lists/List.v')
| -rw-r--r-- | theories/Lists/List.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index f6bd7d1460..5aea97dd6b 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -199,6 +199,14 @@ Section Facts. apply app_cons_not_nil in H1 as []. Qed. + Lemma elt_eq_unit : forall l1 l2 (a b : A), + l1 ++ a :: l2 = [b] -> a = b /\ l1 = [] /\ l2 = []. + Proof. + intros l1 l2 a b Heq. + apply app_eq_unit in Heq. + now destruct Heq as [[Heq1 Heq2]|[Heq1 Heq2]]; inversion_clear Heq2. + Qed. + Lemma app_inj_tail : forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b. Proof. |