This commit is contained in:
Adam Chlipala 2021-03-29 09:28:33 -04:00
parent 75ea3ed0b3
commit 1c69525dc5

View file

@ -1302,7 +1302,7 @@ That is, when $p \in \Gamma$, we have $v(p) = \top$; and when $\neg p \in \Gamma
Given context $\Gamma$ and formula $\phi$, if
\begin{itemize}
\item there is no variable $p$ such that both $p \in \Gamma$ and $\neg p \in \Gamma$, and
\item for any valuation $v$ compatible with $\Gamma$, we have $\denote{p}v$,
\item for any valuation $v$ compatible with $\Gamma$, we have $\denote{\phi}v$,
\end{itemize}
then $\Gamma \vdash \phi$.
\end{lemma}