diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-09-14 23:55:47 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-09-14 23:55:47 -0400 |
| commit | 9c5f398bf0fef00a10a36cdcf09778fe3c31dd9d (patch) | |
| tree | c2f729a8a4e3439d2990b39f6380a693e22f52c9 /src/Util | |
| parent | 8a0551767bdf1c6b8f5c05e50f9722912d4eb98b (diff) | |
Add nth_error_Proper_eqlistA
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 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. |