From 532f6d0a996df45517e623cf403ef8a29595ac84 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 6 Oct 2016 14:41:30 +0200
Subject: [PATCH] docs: intro rule for box
---
docs/base-logic.tex | 1 +
1 file changed, 1 insertion(+)
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 55c7baf02..b13b3c145 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
--
GitLab