diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-10-29 17:26:55 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-10-29 17:26:55 -0400 |
| commit | 949e80041380e69cd455701561cef0088309d7b0 (patch) | |
| tree | 052b6fd45dd8d4f3595d500d42e8104331e4c658 /src/Util | |
| parent | 305f85996292b190247c7b25620f85699c30d44b (diff) | |
Add eqlistA_eq_iff
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ListUtil/SetoidList.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Util/ListUtil/SetoidList.v b/src/Util/ListUtil/SetoidList.v index f620ccc96..59bae9ac4 100644 --- a/src/Util/ListUtil/SetoidList.v +++ b/src/Util/ListUtil/SetoidList.v @@ -23,3 +23,11 @@ Proof. revert ls1 ls2 Hls. induction n; intros ls1 ls2 Hls; destruct Hls; cbn; auto. Qed. + +Lemma eqlistA_eq_iff {A} + : forall ls1 ls2, eqlistA (@eq A) ls1 ls2 <-> ls1 = ls2. +Proof. + induction ls1 as [|x xs IHxs], ls2 as [|y ys IHys]. + all: split; intro H; inversion_clear H; repeat constructor; subst; f_equal; try reflexivity. + apply IHxs; assumption. +Qed. |