From 17bc1af518c668e7b79e1341f005c05553e1e153 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 3 May 2019 15:57:00 +0200
Subject: [PATCH] Some utility lemmas about `dist` on `::`.

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

diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 6e9fac61e..1103c51d7 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -46,6 +46,13 @@ Proof. intros ????; by apply dist_option_Forall2, Forall2_last. Qed.
 Global Instance resize_ne n :
   NonExpansive2 (@resize A n) := _.
 
+Lemma list_dist_cons_inv_l n x l k :
+  x :: l ≡{n}≡ k → ∃ y k', x ≡{n}≡ y ∧ l ≡{n}≡ k' ∧ k = y :: k'.
+Proof. apply Forall2_cons_inv_l. Qed.
+Lemma list_dist_cons_inv_r n l k y :
+  l ≡{n}≡ y :: k → ∃ x l', x ≡{n}≡ y ∧ l' ≡{n}≡ k ∧ l = x :: l'.
+Proof. apply Forall2_cons_inv_r. Qed.
+
 Definition list_ofe_mixin : OfeMixin (list A).
 Proof.
   split.
-- 
GitLab