diff --git a/sofp-src/lyx/sofp-appendices.lyx b/sofp-src/lyx/sofp-appendices.lyx
index 05a7abadc..83e066bac 100644
--- a/sofp-src/lyx/sofp-appendices.lyx
+++ b/sofp-src/lyx/sofp-appendices.lyx
@@ -38043,7 +38043,15 @@ If a type constructor
 \begin_inset Formula $P$
 \end_inset
 
- is lifting-to-full then 
+ is lifting-to-full and not identically void (
+\begin_inset Formula $P^{A}\neq\bbnum 0$
+\end_inset
+
+ for some type 
+\begin_inset Formula $A$
+\end_inset
+
+) then 
 \begin_inset Formula $P$
 \end_inset