diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 69dc87bfea835542094e3545a8dfddec4bf3efbe..6671535a205186d778bdb4308125051db322466c 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -6,35 +6,31 @@ From iris.base_logic.lib Require Import wsat.
 Set Default Proof Using "Type".
 Import uPred.
 
-
-Lemma fresh_inv_name (E : gset positive) N : âˆƒ i, i âˆ‰ E âˆ§ i âˆˆ (â†‘N:coPset).
-Proof.
-  exists (coPpick (â†‘ N âˆ– gset_to_coPset E)).
-  rewrite -elem_of_gset_to_coPset (comm and) -elem_of_difference.
-  apply coPpick_elem_of=> Hfin.
-  eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
-  apply gset_to_coPset_finite.
-Qed.
+(** Semantic Invariants *)
+Definition inv_def `{!invG Î£} (N : namespace) (P : iProp Î£) : iProp Î£ :=
+  (â–¡ âˆ€ E, âŒœâ†‘N âŠ† EâŒ â†’ |={E,E âˆ– â†‘N}=> â–· P âˆ— (â–· P ={E âˆ– â†‘N,E}=âˆ— True))%I.
+Definition inv_aux : seal (@inv_def). by eexists. Qed.
+Definition inv {Î£ i} := inv_aux.(unseal) Î£ i.
+Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
+Instance: Params (@inv) 3 := {}.
+Typeclasses Opaque inv.
 
 (** * Invariants *)
 Section inv.
   Context `{!invG Î£}.
+  Implicit Types i : positive.
+  Implicit Types N : namespace.
+  Implicit Types E : coPset.
+  Implicit Types P Q R : iProp Î£.
 
-  (** Internal backing store of invariants *)
-  Definition internal_inv_def (N : namespace) (P : iProp Î£) : iProp Î£ :=
+  (** ** Internal model of invariants *)
+  Definition own_inv (N : namespace) (P : iProp Î£) : iProp Î£ :=
     (âˆƒ i P', âŒœi âˆˆ (â†‘N:coPset)âŒ âˆ§ â–· â–¡ (P' â†” P) âˆ§ ownI i P')%I.
-  Definition internal_inv_aux : seal (@internal_inv_def). by eexists. Qed.
-  Definition internal_inv := internal_inv_aux.(unseal).
-  Definition internal_inv_eq : @internal_inv = @internal_inv_def := internal_inv_aux.(seal_eq).
-  Typeclasses Opaque internal_inv.
-
-  Global Instance internal_inv_persistent N P : Persistent (internal_inv N P).
-  Proof. rewrite internal_inv_eq /internal_inv; apply _. Qed.
 
-  Lemma internal_inv_open E N P :
-  â†‘N âŠ† E â†’ internal_inv N P ={E,Eâˆ–â†‘N}=âˆ— â–· P âˆ— (â–· P ={Eâˆ–â†‘N,E}=âˆ— True).
+  Lemma own_inv_open E N P :
+    â†‘N âŠ† E â†’ own_inv N P ={E,Eâˆ–â†‘N}=âˆ— â–· P âˆ— (â–· P ={Eâˆ–â†‘N,E}=âˆ— True).
   Proof.
-    rewrite internal_inv_eq /internal_inv_def uPred_fupd_eq /uPred_fupd_def.
+    rewrite uPred_fupd_eq /uPred_fupd_def.
     iDestruct 1 as (i P') "(Hi & #HP' & #HiP)".
     iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
     rewrite {1 4}(union_difference_L (â†‘ N) E) // ownE_op; last set_solver.
@@ -46,18 +42,27 @@ Section inv.
     iApply "HP'". iFrame.
   Qed.
 
-  Lemma internal_inv_alloc N E P : â–· P ={E}=âˆ— internal_inv N P.
+  Lemma fresh_inv_name (E : gset positive) N : âˆƒ i, i âˆ‰ E âˆ§ i âˆˆ (â†‘N:coPset).
+  Proof.
+    exists (coPpick (â†‘ N âˆ– gset_to_coPset E)).
+    rewrite -elem_of_gset_to_coPset (comm and) -elem_of_difference.
+    apply coPpick_elem_of=> Hfin.
+    eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
+    apply gset_to_coPset_finite.
+  Qed.
+
+  Lemma own_inv_alloc N E P : â–· P ={E}=âˆ— own_inv N P.
   Proof.
-    rewrite internal_inv_eq /internal_inv_def uPred_fupd_eq. iIntros "HP [Hw $]".
+    rewrite uPred_fupd_eq. iIntros "HP [Hw $]".
     iMod (ownI_alloc (.âˆˆ (â†‘N : coPset)) P with "[$HP $Hw]")
       as (i ?) "[$ ?]"; auto using fresh_inv_name.
     do 2 iModIntro. iExists i, P. rewrite -(iff_refl True%I). auto.
   Qed.
 
-  Lemma internal_inv_alloc_open N E P :
-    â†‘N âŠ† E â†’ (|={E, Eâˆ–â†‘N}=> internal_inv N P âˆ— (â–·P ={Eâˆ–â†‘N, E}=âˆ— True))%I.
+  Lemma own_inv_alloc_open N E P :
+    â†‘N âŠ† E â†’ (|={E, Eâˆ–â†‘N}=> own_inv N P âˆ— (â–·P ={Eâˆ–â†‘N, E}=âˆ— True))%I.
   Proof.
-    rewrite internal_inv_eq /internal_inv_def uPred_fupd_eq. iIntros (Sub) "[Hw HE]".
+    rewrite uPred_fupd_eq. iIntros (Sub) "[Hw HE]".
     iMod (ownI_alloc_open (.âˆˆ (â†‘N : coPset)) P with "Hw")
       as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
     iAssert (ownE {[i]} âˆ— ownE (â†‘ N âˆ– {[i]}) âˆ— ownE (E âˆ– â†‘ N))%I
@@ -75,85 +80,62 @@ Section inv.
     rewrite assoc_L -!union_difference_L //; set_solver.
   Qed.
 
-  (** Invariants API *)
-  Definition inv_def (N: namespace) (P: iProp Î£) : iProp Î£ :=
-    (â–¡ (âˆ€ E, âŒœâ†‘N âŠ† EâŒ â†’ |={E,E âˆ– â†‘N}=> â–· P âˆ— (â–· P ={E âˆ– â†‘N,E}=âˆ— True)))%I.
-  Definition inv_aux : seal (@inv_def). by eexists. Qed.
-  Definition inv := inv_aux.(unseal).
-  Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
-  Typeclasses Opaque inv.
+  Lemma own_inv_to_inv M P: own_inv M P  -âˆ— inv M P.
+  Proof.
+    iIntros "#I". rewrite inv_eq. iIntros (E H).
+    iPoseProof (own_inv_open with "I") as "H"; eauto.
+  Qed.
 
-  (** Properties about invariants *)
-  Global Instance inv_contractive N: Contractive (inv N).
+  (** ** Public API of invariants *)
+  Global Instance inv_contractive N : Contractive (inv N).
   Proof. rewrite inv_eq. solve_contractive. Qed.
 
   Global Instance inv_ne N : NonExpansive (inv N).
   Proof. apply contractive_ne, _. Qed.
 
-  Global Instance inv_proper N: Proper (equiv ==> equiv) (inv N).
+  Global Instance inv_proper N : Proper (equiv ==> equiv) (inv N).
   Proof. apply ne_proper, _. Qed.
 
-  Global Instance inv_persistent M P: Persistent (inv M P).
-  Proof. rewrite inv_eq. typeclasses eauto. Qed.
+  Global Instance inv_persistent N P : Persistent (inv N P).
+  Proof. rewrite inv_eq. apply _. Qed.
 
   Lemma inv_acc N P Q:
     inv N P -âˆ— â–· â–¡ (P -âˆ— Q âˆ— (Q -âˆ— P)) -âˆ— inv N Q.
   Proof.
-    iIntros "#I #Acc". rewrite inv_eq.
-    iModIntro. iIntros (E H). iDestruct ("I" $! E H) as "#I'".
-    iApply fupd_wand_r. iFrame "I'".
-    iIntros "(P & Hclose)". iSpecialize ("Acc" with "P").
-    iDestruct "Acc" as "[Q CB]". iFrame.
-    iIntros "Q". iApply "Hclose". now iApply "CB".
+    rewrite inv_eq. iIntros "#HI #Acc !>" (E H).
+    iMod ("HI" $! E H) as "[HP Hclose]".
+    iDestruct ("Acc" with "HP") as "[$ HQP]".
+    iIntros "!> HQ". iApply "Hclose". iApply "HQP". done.
   Qed.
 
   Lemma inv_iff N P Q : â–· â–¡ (P â†” Q) -âˆ— inv N P -âˆ— inv N Q.
   Proof.
-    iIntros "#HPQ #I". iApply (inv_acc with "I").
-    iNext. iIntros "!# P". iSplitL "P".
+    iIntros "#HPQ #HI". iApply (inv_acc with "HI").
+    iIntros "!> !# HP". iSplitL "HP".
     - by iApply "HPQ".
-    - iIntros "Q". by iApply "HPQ".
-  Qed.
-
-  Lemma inv_to_inv M P: internal_inv M P  -âˆ— inv M P.
-  Proof.
-    iIntros "#I". rewrite inv_eq. iIntros (E H).
-    iPoseProof (internal_inv_open with "I") as "H"; eauto.
+    - iIntros "HQ". by iApply "HPQ".
   Qed.
 
   Lemma inv_alloc N E P : â–· P ={E}=âˆ— inv N P.
   Proof.
-    iIntros "P". iPoseProof (internal_inv_alloc  N E with "P") as "I".
-    iApply fupd_mono; last eauto.
-    iApply inv_to_inv.
+    iIntros "HP". iApply own_inv_to_inv.
+    iApply (own_inv_alloc N E with "HP").
   Qed.
 
   Lemma inv_alloc_open N E P :
     â†‘N âŠ† E â†’ (|={E, Eâˆ–â†‘N}=> inv N P âˆ— (â–·P ={Eâˆ–â†‘N, E}=âˆ— True))%I.
   Proof.
-    iIntros (H). iPoseProof (internal_inv_alloc_open _ _ _ H) as "H".
-    iApply fupd_mono; last eauto.
-    iIntros "[I H]"; iFrame; by iApply inv_to_inv.
+    iIntros (?). iMod own_inv_alloc_open as "[HI $]"; first done.
+    iApply own_inv_to_inv. done.
   Qed.
 
   Lemma inv_open E N P :
     â†‘N âŠ† E â†’ inv N P ={E,Eâˆ–â†‘N}=âˆ— â–· P âˆ— (â–· P ={Eâˆ–â†‘N,E}=âˆ— True).
   Proof.
-    rewrite inv_eq /inv_def; iIntros (H) "#I". by iApply "I".
-  Qed.
-
-  Lemma inv_open_strong E N P :
-    â†‘N âŠ† E â†’ inv N P ={E,Eâˆ–â†‘N}=âˆ— â–· P âˆ— âˆ€ E', â–· P ={E',â†‘N âˆª E'}=âˆ— True.
-  Proof.
-      iIntros (?) "Hinv".      iPoseProof (inv_open (â†‘ N) N P with "Hinv") as "H"; first done.
-      rewrite difference_diag_L.
-      iPoseProof (fupd_mask_frame_r _ _ (E âˆ– â†‘ N) with "H") as "H"; first set_solver.
-      rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
-      iIntros (E') "HP".
-      iPoseProof (fupd_mask_frame_r _ _ E' with "(H HP)") as "H"; first set_solver.
-        by rewrite left_id_L.
+    rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI".
   Qed.
 
+  (** ** Proof mode integration *)
   Global Instance into_inv_inv N P : IntoInv (inv N P) N := {}.
 
   Global Instance into_acc_inv N P E:
@@ -165,6 +147,20 @@ Section inv.
     iIntros (?) "#Hinv _". iApply "Hinv"; done.
   Qed.
 
+  (** ** Derived properties *)
+  Lemma inv_open_strong E N P :
+    â†‘N âŠ† E â†’ inv N P ={E,Eâˆ–â†‘N}=âˆ— â–· P âˆ— âˆ€ E', â–· P ={E',â†‘N âˆª E'}=âˆ— True.
+  Proof.
+    iIntros (?) "Hinv".
+    iPoseProof (inv_open (â†‘ N) N P with "Hinv") as "H"; first done.
+    rewrite difference_diag_L.
+    iPoseProof (fupd_mask_frame_r _ _ (E âˆ– â†‘ N) with "H") as "H"; first set_solver.
+    rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
+    iIntros (E') "HP".
+    iPoseProof (fupd_mask_frame_r _ _ E' with "(H HP)") as "H"; first set_solver.
+    by rewrite left_id_L.
+  Qed.
+
   Lemma inv_open_timeless E N P `{!Timeless P} :
     â†‘N âŠ† E â†’ inv N P ={E,Eâˆ–â†‘N}=âˆ— P âˆ— (P ={Eâˆ–â†‘N,E}=âˆ— True).
   Proof.
@@ -172,23 +168,22 @@ Section inv.
     iIntros "!> {$HP} HP". iApply "Hclose"; auto.
   Qed.
 
-  (* Weakening of semantic invariants *)
-  Lemma inv_proj_l N P Q: inv N (P âˆ— Q) -âˆ— inv N P.
+  Lemma inv_sep_l N P Q : inv N (P âˆ— Q) -âˆ— inv N P.
   Proof.
-    iIntros "#I". iApply inv_acc; eauto.
-    iNext. iIntros "!# [$ Q] P"; iFrame.
+    iIntros "#HI". iApply inv_acc; eauto.
+    iIntros "!> !# [$ $] $".
   Qed.
 
-  Lemma inv_proj_r N P Q: inv N (P âˆ— Q) -âˆ— inv N Q.
+  Lemma inv_sep_r N P Q : inv N (P âˆ— Q) -âˆ— inv N Q.
   Proof.
-    rewrite (bi.sep_comm P Q). eapply inv_proj_l.
+    rewrite (comm _ P Q). eapply inv_sep_l.
   Qed.
 
-  Lemma inv_split N P Q: inv N (P âˆ— Q) -âˆ— inv N P âˆ— inv N Q.
+  Lemma inv_sep N P Q : inv N (P âˆ— Q) -âˆ— inv N P âˆ— inv N Q.
   Proof.
     iIntros "#H".
-    iPoseProof (inv_proj_l with "H") as "$".
-    iPoseProof (inv_proj_r with "H") as "$".
+    iPoseProof (inv_sep_l with "H") as "$".
+    iPoseProof (inv_sep_r with "H") as "$".
   Qed.
 
 End inv.