diff --git a/tex/program-logic.tex b/tex/program-logic.tex
index 338acd4caec5a3e2edf9ef37ee577dca71930a1c..73ced65c11f5c734d0e8cab7746f7342df0db3ad 100644
--- a/tex/program-logic.tex
+++ b/tex/program-logic.tex
@@ -47,6 +47,9 @@ The following proposition states that an invariant with name $\iname$ exists and
 Next, we define \emph{fancy updates}, which are essentially the same as the basic updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
 \[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop) \]
 Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update.
+Masks are sets of natural numbers, \ie they are subsets of $\mathbb{N}$.%
+\footnote{Actually, in the Coq development masks are restricted to a class of sets of natural numbers that contains all finite sets and is closed under union, intersection, difference and complement.
+The restriction is necessary for engineering reasons to still obtain representation independence: two masks should be \emph{definitionally} equal iff they contain the same invariant names.}
 We use $\top$ as symbol for the largest possible mask, $\nat$, and $\bot$ for the smallest possible mask $\emptyset$.
 We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$.
 %