From 9c5f398bf0fef00a10a36cdcf09778fe3c31dd9d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 14 Sep 2018 23:55:47 -0400 Subject: Add nth_error_Proper_eqlistA --- 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 dd89b65a9..f620ccc96 100644 --- a/src/Util/ListUtil/SetoidList.v +++ b/src/Util/ListUtil/SetoidList.v @@ -15,3 +15,11 @@ Proof. intros i; specialize (H (S i)). assumption. Qed. + +Lemma nth_error_Proper_eqlistA {T R} + : Proper (eqlistA R ==> eq ==> option_eq R) (@nth_error T). +Proof. + intros ls1 ls2 Hls n n' ?; subst n'. + revert ls1 ls2 Hls. + induction n; intros ls1 ls2 Hls; destruct Hls; cbn; auto. +Qed. -- cgit v1.2.3