Commit 8d0ef7c5 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso

Label new rule

If Ralf didn't know it, I guess it deserves a name. This is the first I got,
feel free to improve.
parent c02adf58
......@@ -64,7 +64,7 @@ In other words, when working below the except-0 modality, we can \emph{strip
away} the later from timeless propositions. In fact, we can strip away later
from timeless propositions even when working under the later modality:
\begin{mathpar}
\infer{\timeless{\prop} \and \prop \proves \later \propB}
\inferH{later-timeless-strip}{\timeless{\prop} \and \prop \proves \later \propB}
{\later\prop \proves \later\propB}
\end{mathpar}
This rule looks different from the above ones, because we still do not have that
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment