diff --git a/docs/derived.tex b/docs/derived.tex
index 16c615a74f9fb7eeb2952e7623d1415971765b34..0560bc0ebbd83eb0bf443c13351605b040e3dd04 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -244,8 +244,6 @@ Let $\namesp \ni \textlog{InvNamesp} \eqdef \textlog{list}(\textlog{InvName})$ b
 Notice that there is an injection $\textlog{namesp\_inj}: \textlog{InvNamesp} \ra \textlog{InvName}$.
 Whenever needed (in particular, for masks at view shifts and Hoare triples), we coerce $\namesp$ to its suffix-closure: \[\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}\]
 We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$.
-We will overload the usual Iris notation for invariant assertions in the following:
-\[ \knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop} \]
 
 We define the inclusion relation on namespaces as $\namesp_1 \sqsubseteq \namesp_2 \Lra \Exists \namesp_3. \namesp_2 = \namesp_3 \dplus \namesp_1$, \ie $\namesp_1$ is a suffix of $\namesp_2$.
 We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl\namesp_2 \subseteq \namecl\namesp_1$.
@@ -253,7 +251,32 @@ We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl\namesp_2 \subseteq \na
 Similarly, we define $\namesp_1 \sep \namesp_2 \eqdef   \Exists \namesp_1', \namesp_2'. \namesp_1' \sqsubseteq \namesp_1 \land \namesp_2' \sqsubseteq \namesp_2 \land |\namesp_1'| = |\namesp_2'| \land \namesp_1' \neq \namesp_2'$, \ie there exists a distinguishing suffix.
 We have that $\namesp_1 \sep \namesp_2 \Ra \namecl\namesp_2 \sep \namecl\namesp_1$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \sep \namesp.\iname_2$.
 
-\ralf{Give derived rules for invariants.}
+We will overload the usual Iris notation for invariant assertions in the following:
+\[ \knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop} \]
+We can now derive the following rules for this derived form of the invariant assertion:
+\begin{mathpar}
+  \axiom{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop}
+
+  \axiom{\later\prop \proves \pvs[\namesp] \knowInv\namesp\prop}
+
+  \infer{\physatomic{\expr} \and \namesp \subseteq \mask \and
+    \pfctx \proves \knowInv\namesp\prop \and
+    \pfctx \proves \later\prop \wand \wpre\expr[\mask \setminus \namesp]{\Ret\val.\later\prop * \propB}}
+  {\pfctx \proves \wpre\expr[\mask]{\Ret\val.\propB}}
+
+  \infer{\namesp \subseteq \mask \and
+    \pfctx \proves \knowInv\namesp\prop \and
+    \pfctx \proves \later\prop \wand \pvs[\mask \setminus \namesp]{\later\prop * \propB}}
+  {\pfctx \proves \pvs[\mask]{\propB}}
+
+  \infer{\physatomic{\expr} \and \namesp \subseteq \mask \and
+    \hoare{\later\prop*\propB}\expr{\Ret\val.\later\prop*\propC}[\mask \setminus \namesp]}
+  {\knowInv\namesp\prop \proves \hoare\propB\expr{\Ret\val.\propC}[\mask]}
+
+  \infer{\namesp \subseteq \mask \and
+    \later\prop*\propB \vs[\mask \setminus \namesp] \later\prop*\propC}
+  {\knowInv\namesp\prop \proves \propB \vs[\mask] \propC}
+\end{mathpar}
 
 % \subsection{STSs with interpretation}\label{sec:stsinterp}
 
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 9f124b2d019f699a6744c56fb1e3233fa6a1de3d..fe7966622089e8d2c26f024d757d0e55e4674f70 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -113,4 +113,19 @@ Proof.
   rewrite (comm _ _ (â–· R)%I); setoid_rewrite (comm _ _ R).
   apply ht_frame_step_l.
 Qed.
+
+Lemma ht_inv N E P Φ R e :
+  atomic e → nclose N ⊆ E →
+  (inv N R ★ {{ ▷ R ★ P }} e @ E ∖ nclose N {{ λ v, ▷ R ★ Φ v }})
+    ⊢ {{ P }} e @ E {{ Φ }}.
+Proof.
+  intros; apply: always_intro. apply impl_intro_l.
+  rewrite always_and_sep_r assoc [(P ★ _)%I]comm -assoc.
+  eapply wp_inv; [by eauto with I..|].
+  rewrite sep_elim_r. apply wand_intro_l.
+  (* Oh wow, this is annyoing... *)
+  rewrite assoc -always_and_sep_r'.
+  by rewrite /ht always_elim impl_elim_r.
+Qed.
+
 End hoare.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index dd1978f4c4eeea4502cfd2d1ff26b30702c11f6d..0035924cb739fab3581764be7445758b032c735b 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -54,14 +54,14 @@ Qed.
 
 (* Derive the concrete forms for pvs and wp, because they are useful. *)
 
-Lemma pvs_open_close E N P Q R :
+Lemma pvs_inv E N P Q R :
   nclose N ⊆ E →
   R ⊢ inv N P →
   R ⊢ (▷ P -★ |={E ∖ nclose N}=> (▷ P ★ Q)) →
   R ⊢ (|={E}=> Q).
 Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
 
-Lemma wp_open_close E e N P Φ R :
+Lemma wp_inv E e N P Φ R :
   atomic e → nclose N ⊆ E →
   R ⊢ inv N P →
   R ⊢ (▷ P -★ WP e @ E ∖ nclose N {{ λ v, ▷ P ★ Φ v }}) →
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 639e34a687e4c5156d5f60287be5aa060f9e9c2f..001ec782667d4e0436774b78fa0f6755d7cba99c 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -87,13 +87,13 @@ Qed.
 Lemma vs_mask_frame' E Ef P Q : Ef ∩ E = ∅ → (P ={E}=> Q) ⊢ (P ={E ∪ Ef}=> Q).
 Proof. intros; apply vs_mask_frame; set_solver. Qed.
 
-Lemma vs_open_close N E P Q R :
+Lemma vs_inv N E P Q R :
   nclose N ⊆ E →
   (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊢ (P ={E}=> Q).
 Proof.
   intros; apply: always_intro. apply impl_intro_l.
   rewrite always_and_sep_r assoc [(P ★ _)%I]comm -assoc.
-  eapply pvs_open_close; [by eauto with I..|].
+  eapply pvs_inv; [by eauto with I..|].
   rewrite sep_elim_r. apply wand_intro_l.
   (* Oh wow, this is annyoing... *)
   rewrite assoc -always_and_sep_r'.