diff --git a/program_logic/auth.v b/program_logic/auth.v
index 140232a58bedd8e444a05f621944272a082ac219..4b87e14099f27b5764020df5e61ae587cbc021a7 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -72,15 +72,16 @@ Section auth.
      step-indices. However, since A is timeless, that should not be
      a restriction.  *)
   Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA)
-        `{!LocalUpdate Lv L} E P (Q : X → iPropG Λ Σ) γ a :
+        `{!LocalUpdate Lv L} E P (Q : X → iPropG Λ Σ) R γ a :
     nclose N ⊆ E →
-    (auth_ctx γ ★ auth_own γ a ★ (∀ a', ▷φ (a ⋅ a') -★
-        FSA (E ∖ nclose N) (λ x, ■(Lv a ∧ ✓(L a⋅a')) ★ ▷φ (L a ⋅ a') ★ (auth_own γ (L a) -★ Q x))))
-      ⊑ FSA E Q.
+    R ⊑ auth_ctx γ →
+    R ⊑ (auth_own γ a ★ (∀ a', ▷φ (a ⋅ a') -★
+        FSA (E ∖ nclose N) (λ x, ■(Lv a ∧ ✓(L a⋅a')) ★ ▷φ (L a ⋅ a') ★ (auth_own γ (L a) -★ Q x)))) →
+    R ⊑ FSA E Q.
   Proof.
-    rewrite /auth_ctx=>HN.
-    rewrite -inv_fsa; last eassumption.
-    apply sep_mono; first done. apply wand_intro_l.
+    rewrite /auth_ctx=>HN Hinv Hinner.
+    eapply inv_fsa; [eassumption..|]. rewrite Hinner=>{Hinner Hinv R}.
+    apply wand_intro_l.
     rewrite assoc auth_opened !pvs_frame_r !sep_exist_r.
     apply fsa_strip_pvs; first done. apply exist_elim=>a'.
     rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]comm.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index e2190a870eb8f00ead78fc5953c56f8998e00872..608075029a37124e45b6b648373cd89d6b8b52bb 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -66,12 +66,14 @@ Proof. by rewrite always_always. Qed.
 
 (** Invariants can be opened around any frame-shifting assertion. *)
 Lemma inv_fsa {A : Type} {FSA} (FSAs : FrameShiftAssertion (A:=A) FSA)
-      E N P (Q : A → iProp Λ Σ) :
+      E N P (Q : A → iProp Λ Σ) R :
   nclose N ⊆ E →
-  (inv N P ★ (▷P -★ FSA (E ∖ nclose N) (λ a, ▷P ★ Q a))) ⊑ FSA E Q.
+  R ⊑ inv N P →
+  R ⊑ (▷P -★ FSA (E ∖ nclose N) (λ a, ▷P ★ Q a)) →
+  R ⊑ FSA E Q.
 Proof.
-  move=>HN.
-  rewrite /inv sep_exist_r. apply exist_elim=>i.
+  move=>HN Hinv Hinner. rewrite -[R](idemp (∧)%I) {1}Hinv Hinner =>{Hinv Hinner R}.
+  rewrite always_and_sep_l /inv sep_exist_r. apply exist_elim=>i.
   rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN.
   rewrite -(fsa_trans3 E (E ∖ {[encode i]})) //; last by solve_elem_of+.
   (* Add this to the local context, so that solve_elem_of finds it. *)
@@ -87,16 +89,20 @@ Qed.
 
 (* Derive the concrete forms for pvs and wp, because they are useful. *)
 
-Lemma pvs_open_close E N P Q :
+Lemma pvs_open_close E N P Q R :
   nclose N ⊆ E →
-  (inv N P ★ (▷P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷P ★ Q))) ⊑ pvs E E Q.
-Proof. move=>HN. by rewrite (inv_fsa pvs_fsa). Qed.
+  R ⊑ inv N P →
+  R ⊑ (▷P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷P ★ Q)) →
+  R ⊑ pvs E E Q.
+Proof. move=>HN ? ?. apply: (inv_fsa pvs_fsa); eassumption. Qed.
 
-Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) :
+Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) R :
   atomic e → nclose N ⊆ E →
-  (inv N P ★ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v))) ⊑ wp E e Q.
+  R ⊑ inv N P →
+  R ⊑ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v)) →
+  R ⊑ wp E e Q.
 Proof.
-  move=>He HN. by rewrite (inv_fsa (wp_fsa e _)). Qed.
+  move=>He HN ? ?. apply: (inv_fsa (wp_fsa e _)); eassumption. Qed.
 
 Lemma inv_alloc N P : ▷ P ⊑ pvs N N (inv N P).
 Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index eba86d1c8b768ccabcf720ce9a834bf710a4c890..32a0324c08d0f64c9b85f4087fbc8d169f4ef2f0 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -92,8 +92,8 @@ Lemma vs_open_close N E P Q R :
 Proof.
   intros; apply (always_intro _ _), impl_intro_l.
   rewrite always_and_sep_r assoc [(P ★ _)%I]comm -assoc.
-  rewrite -(pvs_open_close E N) //. apply sep_mono; first done.
-  apply wand_intro_l.
+  apply: (pvs_open_close E N); [by eauto using sep_elim_l..|].
+  rewrite sep_elim_r. apply wand_intro_l.
   (* Oh wow, this is annyoing... *)
   rewrite assoc -always_and_sep_r'.
   by rewrite /vs always_elim impl_elim_r.