diff --git a/docs/base-logic.tex b/docs/base-logic.tex index 55c7baf02f8fd36e2bc7035750ee823e9cb8472e..b13b3c145383955f6959ee28ce588b897bc36d0f 100644 --- a/docs/base-logic.tex +++ b/docs/base-logic.tex @@ -310,6 +310,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda {\always{\prop} \proves \always{\propB}} \and \begin{array}[c]{rMcMl} + \TRUE &\proves& \always{\TRUE} \\ \always{\prop} &\proves& \prop \\ \always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\ \always{\prop} \land \propB &\proves& \always{\prop} * \propB