diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 8c5aa2726c7f443eb46060950678aa7790f676d8..66a05ce0c13b91a52153732b51f404f05af821ef 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.