diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 248d6dbd5251c43fa81c0f05e40430cf00c0249e..0aaa353d3e3b9448c95464273984574514748342 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -62,7 +62,7 @@ Section proofs.
 
   (*** Allocation rules. *)
   (** The "strong" variants permit any infinite [I], and choosing [P] is delayed
-  until after [γ] was chosen. *)
+  until after [γ] was chosen.*)
   Lemma cinv_alloc_strong (I : gname → Prop) E N :
     pred_infinite I →
     (|={E}=> ∃ γ, ⌜ I γ ⌝ ∗ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P)%I.
@@ -73,7 +73,8 @@ Section proofs.
   Qed.
 
   (** The "open" variants create the invariant in the open state, and delay
-  having to prove [P]. *)
+  having to prove [P].
+  These do not imply the other variants because of the extra assumption [↑N ⊆ E]. *)
   Lemma cinv_alloc_strong_open (I : gname → Prop) E N :
     pred_infinite I →
     ↑N ⊆ E →
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 320f7fc86036ff658ae14fdb2a9f3ba3cb847be1..e14ca49393aa0fc8ce0771b26315d9f40604a70b 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -56,6 +56,7 @@ Section inv.
     do 2 iModIntro. iExists i. auto.
   Qed.
 
+  (* This does not imply [own_inv_alloc] due to the extra assumption [↑N ⊆ E]. *)
   Lemma own_inv_alloc_open N E P :
     ↑N ⊆ E → (|={E, E∖↑N}=> own_inv N P ∗ (▷P ={E∖↑N, E}=∗ True))%I.
   Proof.