diff --git a/theories/lib/list.v b/theories/lib/list.v
index 72f7f4d8c10a0b54b9b494b894edeea56dea1595..9f608a56d026ba01b9b22ff1d9e0821625c76177 100644
--- a/theories/lib/list.v
+++ b/theories/lib/list.v
@@ -37,8 +37,8 @@ Proof.
 Qed.
 
 Lemma lrel_list_cons `{relocG Σ} (A : lrel Σ) v1 v2 ls1 ls2 :
-  A v1 v2 -∗
-  lrel_list A ls1 ls2 -∗
+  ▷ A v1 v2 -∗
+  ▷ lrel_list A ls1 ls2 -∗
   lrel_list A (CONSV v1 ls1) (CONSV v2 ls2).
 Proof.
   iIntros "#HA #Hls".