diff --git a/docs/base-logic.tex b/docs/base-logic.tex index d40973e93ee35a9b9c47b86292df61bef563e286..0f7cf136d18eca4451c051bb6421dee38519264f 100644 --- a/docs/base-logic.tex +++ b/docs/base-logic.tex @@ -339,12 +339,12 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda \begin{array}[c]{rMcMl} \All x. \later\prop &\proves& \later{\All x.\prop} \\ \later\Exists x. \prop &\proves& \later\FALSE \lor {\Exists x.\later\prop} \\ - \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop) \\ + \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop) \end{array} \and \begin{array}[c]{rMcMl} \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\ - \always{\later\prop} &\provesIff& \later\always{\prop} \\ + \always{\later\prop} &\provesIff& \later\always{\prop} \end{array} \end{mathpar}