From 315fcfabc46b2f24b005da9d090d0a2b2c69ed03 Mon Sep 17 00:00:00 2001 From: Andrej Dudenhefner <mrhaandi@gmail.com> Date: Thu, 7 Jul 2022 15:10:37 +0200 Subject: [PATCH] prepare for https://github.com/coq/coq/pull/16289 --- theories/list.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/list.v b/theories/list.v index 20135cbb..d7024602 100644 --- a/theories/list.v +++ b/theories/list.v @@ -528,7 +528,7 @@ Proof. revert i. induction l; intros [|?] ?; naive_solver auto with arith. Qed. Lemma lookup_lt_is_Some_1 l i : is_Some (l !! i) → i < length l. Proof. intros [??]; eauto using lookup_lt_Some. Qed. Lemma lookup_lt_is_Some_2 l i : i < length l → is_Some (l !! i). -Proof. revert i. induction l; intros [|?] ?; naive_solver eauto with lia. Qed. +Proof. revert i. induction l; intros [|?] ?; naive_solver auto with lia. Qed. Lemma lookup_lt_is_Some l i : is_Some (l !! i) ↔ i < length l. Proof. split; auto using lookup_lt_is_Some_1, lookup_lt_is_Some_2. Qed. Lemma lookup_ge_None l i : l !! i = None ↔ length l ≤ i. -- GitLab