From e742c4b29ccb930da6040d6951677b366a822927 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 Oct 2023 10:19:29 +0200
Subject: [PATCH] Add instance `cons_dist_inj`.

---
 iris/algebra/list.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 8c5aa2726..66a05ce0c 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -41,6 +41,10 @@ Global Instance last_ne : NonExpansive (@last A).
 Proof. intros ????; by apply dist_option_Forall2, Forall2_last. Qed.
 Global Instance resize_ne n : NonExpansive2 (@resize A n) := _.
 
+Global Instance cons_dist_inj n :
+  Inj2 (dist n) (dist n) (dist n) (@cons A).
+Proof. by inversion_clear 1. Qed.
+
 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.
-- 
GitLab