From 949e80041380e69cd455701561cef0088309d7b0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 29 Oct 2018 17:26:55 -0400 Subject: Add eqlistA_eq_iff --- src/Util/ListUtil/SetoidList.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/Util') 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. -- cgit v1.2.3