 Let \(\mathcal{K}\) be a Kripke model based on a frame in which we have two stages \(s_0 \preceq s_1\). Assume \(\{d \}\) is the domain associated to each stage by the model, and let a monadic predicate \(P\) be true of \(d\) at \(s_1\) but not at \(s_0\). We may verify that \(\neg \forall x \neg Px\) is true at \(s_0\), even though \(\exists x Px\) is not true at \(s_0\). So, (i) is not intuitionistically valid. One may likewise verify that \(\lnot \lnot \forall x Px\) is true at \(s_0\), even though \(\forall x Px\) is not true at \(s_0\). It follows that (ii) is not intuitionistically valid either.