diff --git a/docs/derived.tex b/docs/derived.tex
index 60afd02e53f6f1aa66fcf741eb840dad4507d6fd..df80640344bc8282f48d1f01beed61dc50a2fa45 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -202,6 +202,18 @@ The following rules can be derived for Hoare triples.
 \inferH{Ht-false}
   {}
   {\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]}
+\and
+\inferH{Ht-inv}
+  {\hoare{\later\propC*\prop}{\expr}{\Ret\val.\later\propC*\propB}[\mask] \and
+   \physatomic{\expr}
+  }
+  {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]}
+\and
+\inferH{Ht-inv-timeless}
+  {\hoare{\propC*\prop}{\expr}{\Ret\val.\propC*\propB}[\mask] \and
+   \physatomic{\expr} \and \timeless\propC
+  }
+  {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]}
 \end{mathparpagebreakable}
 
 \paragraph{Lifting of operational semantics.}