diff --git a/docs/derived.tex b/docs/derived.tex
index 696be132bc318fb8d6f73ab3350b1ba92bd16c28..8fa3c08cdc3127bcf5ba551db4bcdd4e762f1d4f 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -176,8 +176,8 @@ The following rules can be derived for Hoare triples.
   {\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask]}
 \and
 \inferH{Ht-frame-step}
-  {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \toval(\expr) = \bot}
-  {\hoare{\prop * \later\propC}{\expr}{\Ret\val. \propB * \propC}[\mask]}
+  {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \toval(\expr) = \bot \and \mask_2 \subseteq \mask_2 \\\\ \propC_1 \vs[\mask_1][\mask_2] \later\propC_2 \and \propC_2 \vs[\mask_2][\mask_1] \propC_3}
+  {\hoare{\prop * \propC_1}{\expr}{\Ret\val. \propB * \propC_3}[\mask \uplus \mask_1]}
 \and
 \inferH{Ht-atomic}
   {\prop \vs[\mask \uplus \mask'][\mask] \prop' \\
diff --git a/docs/logic.tex b/docs/logic.tex
index 7e17741b50d85b4aac5ece5009d1687fdaca6c13..24a8ca03a3b930e2aa59ea06e32d44bfc309a6bb 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -584,8 +584,8 @@ This is entirely standard.
 {}{\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}}
 
 \infer[wp-frame-step]
-{\toval(\expr) = \bot}
-{\later\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}}
+{\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1}
+{\wpre\expr[\mask]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2]\later\pvs[\mask_2][\mask_1]\propB \proves \wpre\expr[\mask \uplus \mask_1]{\Ret\var.\propB*\prop}}
 
 \infer[wp-bind]
 {\text{$\lctx$ is a context}}