From b66b531172a20ad19cf3ddf405cdaf9ce5f18e5b Mon Sep 17 00:00:00 2001
From: Jonas Kastberg <jihgfee@gmail.com>
Date: Fri, 14 Jan 2022 11:58:43 +0000
Subject: [PATCH] Add `last_cons_Some_ne` lemma for the `last` function

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

diff --git a/theories/list.v b/theories/list.v
index c00e8dc1..b6a72eac 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1151,6 +1151,9 @@ Qed.
 Lemma last_cons x l :
   last (x :: l) = match last l with Some y => Some y | None => Some x end.
 Proof. by apply (last_app [x]). Qed.
+Lemma last_cons_Some_ne x y l :
+  x ≠ y → last (x :: l) = Some y → last l = Some y.
+Proof. rewrite last_cons. destruct (last l); naive_solver. Qed.
 Lemma last_lookup l : last l = l !! pred (length l).
 Proof. by induction l as [| ?[]]. Qed.
 Lemma last_reverse l : last (reverse l) = head l.
-- 
GitLab