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 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. |