From f4f0f216c608ad0443f6e3180a2d1de3a38193e0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Jan 2020 22:48:22 +0100
Subject: [PATCH] Lemma for lookup of cons.

---
 theories/list.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index 722c20ff..8bcead87 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -482,6 +482,8 @@ Lemma nil_or_length_pos l : l = [] ∨ length l ≠ 0.
 Proof. destruct l; simpl; auto with lia. Qed.
 Lemma nil_length_inv l : length l = 0 → l = [].
 Proof. by destruct l. Qed.
+Lemma lookup_cons_ne_0 l x i : i ≠ 0 → (x :: l) !! i = l !! pred i.
+Proof. by destruct i. Qed.
 Lemma lookup_nil i : @nil A !! i = None.
 Proof. by destruct i. Qed.
 Lemma lookup_tail l i : tail l !! i = l !! S i.
-- 
GitLab