diff --git a/docs/logic.tex b/docs/logic.tex index d2d84550b2b395d546ad9fc6db2b3ed059cfc051..a2c4e4fd400371e6646609516e4c782fa507a66a 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -498,8 +498,8 @@ A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ i {\always{\prop} \proves \prop} \and \begin{array}[c]{rMcMl} - \always{(\prop * \propB)} &\proves& \always{(\prop \land \propB)} \\ - \always{\prop} * \propB &\proves& \always{\prop} \land \propB \\ + \always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\ + \always{\prop} \land \propB &\proves& \always{\prop} * \propB \\ \always{\later\prop} &\provesIff& \later\always{\prop} \\ \end{array} \and