diff options
Diffstat (limited to 'src/Util/ListUtil/SetoidList.v')
| -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. |