diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index d6d711649ccb1b43799f4116b2adaff5527cc578..354d342f7ee9349ebfa9712cdfe2823299527071 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -434,7 +434,7 @@ We can now derive the following rules (this involves unfolding the definition of
 \begin{mathpar}
   \axiomH{inv-persist}{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop}
 
-  \axiomH{inv-alloc}{\later\prop \proves \pvs[\namesp] \knowInv\namesp\prop}
+  \axiomH{inv-alloc}{\later\prop \proves \pvs[\bot] \knowInv\namesp\prop}
 
   \inferH{inv-open}
   {\namesp \subseteq \mask}