non-disjunctive is not identically void

winitzki · Apr 3, 2024 · 66cc810 · 66cc810
1 parent fb129f5
commit 66cc810
Showing 1 changed file with 9 additions and 1 deletion.
diff --git 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