diff options
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 7f5bea670..ba1d8326a 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -223,6 +223,14 @@ Proof. induction n; destruct xs; nth_tac. Qed. +Lemma In_nth_error_value : forall {T} xs (x:T), + In x xs -> exists n, nth_error xs n = Some x. +Proof. + induction xs; nth_tac; break_or_hyp. + - exists 0; reflexivity. + - edestruct IHxs; eauto. exists (S x0). eauto. +Qed. + Lemma nth_value_index : forall {T} i xs (x:T), nth_error xs i = Some x -> In i (seq 0 (length xs)). Proof. |