diff --git a/src/guarding/guard.v b/src/guarding/guard.v
index 4dbcf79..e26863b 100644
--- a/src/guarding/guard.v
+++ b/src/guarding/guard.v
@@ -1332,7 +1332,7 @@ Qed.
 
 (** Guarding and disjunction **)
 
-Lemma lguards_or_with_lhs (P R S : iProp Σ) F n
+Lemma guards_cancel_or_with_lhs (P R S : iProp Σ) F n
     (pr_impl_false: (P ∧ R ⊢ False))
     : (
       (P &&{F; n}&&> (R ∨ S))
@@ -1346,7 +1346,7 @@ Proof.
   iApply lfguards_or_with_lhs; trivial. trivial.
 Qed.
 
-Lemma lguards_exists_with_lhs X (P : iProp Σ) (S R : X -> iProp Σ) F n
+Lemma guards_strengthen_exists_with_lhs X (P : iProp Σ) (S R : X -> iProp Σ) F n
     (pr_impl_s: (∀ x, P ∧ R x ⊢ S x))
     (pers: ∀ x, Persistent (S x))
     : (
@@ -1361,7 +1361,7 @@ Proof.
   iApply lfguards_exists_with_lhs; trivial.
 Qed.
 
-Lemma guards_or (P Q R S : iProp Σ) F1 F2 n
+Lemma guards_cancel_or (P Q R S : iProp Σ) F1 F2 n
     (qrx: (Q ∧ R ⊢ False))
     : (
       (P &&{F1; n}&&> Q) ∗ (P &&{F2; n}&&> (R ∨ S))
@@ -1393,7 +1393,7 @@ Proof.
 
 
 
-Lemma lguards_or_guards_false E P Q S n m :
+Lemma guards_cancel_or_by_chaining_additive E P Q S n m :
     (P &&{ E ; n }&&> Q ∨ S) ∗ (Q &&{ E ; m }&&> False) ⊢ (P &&{ E ; n + m }&&> S).
 Proof.
   rewrite guards_unseal. unfold guards_def.
@@ -1409,10 +1409,10 @@ Proof.
   iPureIntro. set_solver.
 Qed.
 
-Lemma guards_or_guards_false E P Q S :
+Lemma guards_cancel_or_by_chaining E P Q S :
     (P &&{ E }&&> Q ∨ S) ∗ (Q &&{ E }&&> False) ⊢ (P &&{ E }&&> S).
 Proof.
-  apply lguards_or_guards_false.
+  apply guards_cancel_or_by_chaining_additive.
 Qed.
 
 (** The relationship between guarding and invariants **)
diff --git a/src/guarding/lib/lifetime.v b/src/guarding/lib/lifetime.v
index 24f8d1f..0c11ba1 100644
--- a/src/guarding/lib/lifetime.v
+++ b/src/guarding/lib/lifetime.v
@@ -686,7 +686,7 @@ Section LlftLogic.
     { 
       iAssert (llft_alive κ &&{ ↑NLLFT ∪ ↑NLLFT }&&> ▷ P) as "H".
       { iApply
-        (guards_or (llft_alive κ) (llft_alive κ) (llft_dead κ ∗ Cancel γc) (▷ P)).
+        (guards_cancel_or (llft_alive κ) (llft_alive κ) (llft_dead κ ∗ Cancel γc) (▷ P)).
         { iIntros "t". iApply (llftl_not_own_end_and κ). iSplit.
           { iDestruct "t" as "[t _]". iFrame "t". }
           { iDestruct "t" as "[_ [t _]]". iFrame "t". }
@@ -746,7 +746,7 @@ Section LlftLogic.
       }
 
       iAssert (True &&{ ↑NLLFT}&&> (∃ sa sd : gset nat, ⌜κ ⊈ sa⌝ ∗ LtState llft_name sa sd ∗ llft_alive sa)) as "G3".
-        { iApply guards_or_guards_false. iFrame "ctx2". 
+        { iApply guards_cancel_or_by_chaining. iFrame "ctx2". 
           leaf_goal rhs to (llft_alive κ). { iFrame "G2". }
           leaf_by_sep.
           { iIntros "T". 
diff --git a/src/guarding/storage_protocol/protocol.v b/src/guarding/storage_protocol/protocol.v
index a184ca5..59bbce2 100644
--- a/src/guarding/storage_protocol/protocol.v
+++ b/src/guarding/storage_protocol/protocol.v
@@ -467,7 +467,7 @@ Section StorageLogic.
     iDestruct (guards_true E (sp_own γ p)) as "gt".
     iDestruct (guards_transitive _ (sp_own γ p) True%I with "[gt mg]") as "gg".
       { iFrame "gt". iFrame "mg". }
-    iDestruct (lguards_exists_with_lhs (P*B) (sp_own γ p) 
+    iDestruct (guards_strengthen_exists_with_lhs (P*B) (sp_own γ p) 
       (λ (state_t: P*B), (▷ (⌜ p ≼ state_t.1 ⌝))%I)
       (λ (state_t: P*B), (▷ (own γ (● Inved state_t.1) ∗ ⌜sp_rel state_t.1 state_t.2⌝ ∗ f state_t.2))%I)
       E 0