diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 5e7d5418327fbbf5b0bf1c755fa5ba15a46c398b..450b6a6adc6c83a3e6ebbf606b6817c588daa7b2 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -179,7 +179,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
 	\infer{
 		\vctx, \var:\type \proves \wtt{\term}{\type} \and
 		\text{$\var$ is guarded in $\term$} \and
-		\text{$\type$ is complete}
+		\text{$\type$ is complete and inhabited}
 	}{
 		\vctx \proves \wtt{\MU \var:\type. \term}{\type}
 	}