diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index a1af8026d410b62d13f0ff9232f5ff606fd0f020..25bf0a9a6beb394ed42b8c99abcaeec284ec46bc 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -165,22 +165,20 @@ Section inv.
     iIntros "!> {$HP} HP". iApply "Hclose"; auto.
   Qed.
 
-  Lemma inv_sep_l N P Q : inv N (P ∗ Q) -∗ inv N P.
+  Lemma inv_split_l N P Q : inv N (P ∗ Q) -∗ inv N P.
   Proof.
     iIntros "#HI". iApply inv_alter; eauto.
     iIntros "!> !> [$ $] $".
   Qed.
-
-  Lemma inv_sep_r N P Q : inv N (P ∗ Q) -∗ inv N Q.
+  Lemma inv_split_r N P Q : inv N (P ∗ Q) -∗ inv N Q.
   Proof.
-    rewrite (comm _ P Q). eapply inv_sep_l.
+    rewrite (comm _ P Q). eapply inv_split_l.
   Qed.
-
-  Lemma inv_sep N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
+  Lemma inv_split N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
   Proof.
     iIntros "#H".
-    iPoseProof (inv_sep_l with "H") as "$".
-    iPoseProof (inv_sep_r with "H") as "$".
+    iPoseProof (inv_split_l with "H") as "$".
+    iPoseProof (inv_split_r with "H") as "$".
   Qed.
 
 End inv.