diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-01-06 00:46:50 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-01-06 00:46:50 -0500 |
| commit | aebc0124ee411786cd711042da7abb67cdf5b40a (patch) | |
| tree | e055a5d8a314ab0a55ae72456040ad9a25b46220 /src/Util/ListUtil.v | |
| parent | bd39778e0679d1f67b5595e655aba1f62ac14e97 (diff) | |
fix letify to only insert a term once
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 350f55dd8..783e3f527 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -524,3 +524,12 @@ Ltac set_nth_inbounds := end. Ltac nth_inbounds := nth_error_inbounds || set_nth_inbounds. + +Lemma cons_eq_head : forall {T} (x y:T) xs ys, x::xs = y::ys -> x=y. +Proof. + intros; solve_by_inversion. +Qed. +Lemma cons_eq_tail : forall {T} (x y:T) xs ys, x::xs = y::ys -> xs=ys. +Proof. + intros; solve_by_inversion. +Qed. |