prftree (19jun19)

git-svn-id: svn://tug.org/texlive/trunk@51404 c570f23f-e606-0410-a88d-b1316a301751

3 files changed, 1123 insertions, 190 deletions

diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
index 3e4ed547069..5f3b0a615e6 100644
--- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
+++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
index 1fe8d227c6c..19477fa856f 100644
--- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
+++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
@@ -1,8 +1,9 @@
 \documentclass{amsart}
 \usepackage{color}
 \usepackage{graphics}
-\usepackage[ND,SEQ]{prftree}
+\usepackage[ND,SEQ,EQ,ML]{prftree}
 \usepackage{url}
+\usepackage{microtype}
 
 \setlength{\fboxsep}{0pt}
 
@@ -54,7 +55,7 @@ textbooks, e.g., A.S.~Troelstra and H.~Schwichtenberg, \textit{Basic
 % --------------------------
 \clearpage
 \section{Basic Commands}\label{sec:basic_commands}
-The package is invoked by putting \verb|\usepackage{prfree.sty}| in
+The package is invoked by putting \verb|\usepackage{prftree.sty}| in
 the preamble of the document, and installation reduces to put the file
 \texttt{prftree.sty} somewhere in the \LaTeX{} search
 path.\vspace{2ex} 
@@ -157,8 +158,7 @@ left-to-right, so \verb|[d,s]| is the same as \verb|[s]|, while
 \verb|[noline,straight,d]| is the same as \verb|[noline]|.
 
 The conjunction introduction rule illustrates the various line
-options\footnote{The reader is invited to look at the source code of
-  the documentation to see how these examples have been implemented.}:
+options:
 \begin{displaymath}
   \begin{array}{lcc@{\qquad}l}
     \mbox{default (single straight)} &
@@ -207,7 +207,14 @@ options\footnote{The reader is invited to look at the source code of
     {A}{B}{A \wedge B} &
     \texttt{[noline]}
   \end{array}
-\end{displaymath}\vspace{1ex}
+\end{displaymath}
+These examples are implemented in an array whose cells have the form
+\begin{center}
+  \verb|\prftree[|\emph{option}\verb|]{A}{B}{A \wedge B} &|
+  \verb|\prftree[|\emph{option}\verb|,r]{$\scriptstyle\wedge\mathrm{I}$}|
+\end{center}
+in which the option part is the one on the right of the
+picture.\vspace{1ex} 
 
 An assumption is a special proof tree, built by the command:
 \begin{displaymath}
@@ -967,42 +974,128 @@ the last used value.
 The basic commands illustrated so far allow to control proof trees in
 all aspects, but they tend to be verbose in practise. Thus, a number
 of abbreviations are provided to make handier the writing of proofs.
-
 Since they may collide with other packages, these macros are activated
-by suitable options. By loading the package as
-\verb|\usepackage[ND]{prftree.sty}|, the following abbreviations are
-available, which correspond to the inference rule of natural deduction
-calculi:
+by suitable options. Multiple options can be used at the same time.
+
+\subsection{Natural deduction}
+By loading the package with the \verb|ND| option, the following
+abbreviations are available, which correspond to the inference rules
+of natural deduction calculi:
 \begin{itemize}
 \item \verb|\NDA|: assumption;
 \item \verb|\NDAL|: labelled assumption;
-\item \verb|\NDD|: bounded assumption;
-\item \verb|\NDDL|: labelled bounded assumption;
+\item \verb|\NDD|: discharged assumption;
+\item \verb|\NDDL|: labelled discharged assumption;
 \item \verb|\NDP|: generic proof tree;
-\item \verb|\NDANDI|: conjunction introduction;
-\item \verb|\NDANDER|: conjunction elimination, right;
-\item \verb|\NDANDEL|: conjunction elimination, left;
-\item \verb|\NDANDE|: conjunction elimination, unspecified;
-\item \verb|\NDORIR|: disjunction introduction, right;
-\item \verb|\NDORIL|: disjunction introduction, left;
-\item \verb|\NDORI|: disjunction introduction, unspecified;
-\item \verb|\NDORE|: disjunction elimination;
-\item \verb|\NDOREL|: labelled disjunction elimination;
-\item \verb|\NDIMPI|: implication introduction;
-\item \verb|\NDIMPIL|: labelled implication introduction;
-\item \verb|\NDIMPE|: implication elimination;
-\item \verb|\NDNOTI|: negation introduction;
-\item \verb|\NDNOTIL|: labelled negation introduction;
-\item \verb|\NDNOTE|: negation elimination;
-\item \verb|\NDALLI|: universal quantifier introduction;
-\item \verb|\NDALLE|: universal quantifier elimination;
-\item \verb|\NDEXI|: existential quantifier introduction;
-\item \verb|\NDEXE|: existential quantifier elimination;
-\item \verb|\NDEXE|: labelled existential quantifier elimination;
-\item \verb|\NDTI|: truth introduction;
-\item \verb|\NDFE|: falsity elimination;
-\item \verb|\NDLEM|: law of Excluded Middle;
-\item \verb|\NDAX|: a generic axiom rule.
+\item \verb|\NDAX|: a generic axiom rule;
+  \begin{displaymath}
+    \vcenter{\NDAX{x = x}}\enspace;
+  \end{displaymath}
+\item \verb|\NDANDI|: conjunction introduction
+  \begin{displaymath}
+    \vcenter{\NDANDI{\NDA{A}}{\NDA{B}}{A \wedge B}}\enspace;
+  \end{displaymath}
+\item \verb|\NDANDER|, \verb|\NDANDEL|, \verb|\NDANDE|: conjunction
+  elimination right, left, and unspecified, respectively
+  \begin{displaymath}
+    \vcenter{\NDANDEL{\NDA{A \wedge B}}{\NDA{A}}} \quad
+    \vcenter{\NDANDER{\NDA{A \wedge B}}{\NDA{B}}}\enspace;
+  \end{displaymath}
+\item \verb|\NDORIR|, \verb|\NDORIL|, \verb|\NDORI|: disjunction
+  introduction right, left, and unspecified, respectively
+  \begin{displaymath}
+    \vcenter{\NDORIL{\NDA{A}}{\NDA{A \vee B}}} \quad
+    \vcenter{\NDORIR{\NDA{B}}{\NDA{A \vee B}}}\enspace;
+  \end{displaymath}
+\item \verb|\NDOREL|, \verb|\NDORE|: disjunction elimination, possibly
+  labelled 
+  \begin{displaymath}
+    \begin{prfenv}
+      \vcenter{\NDOREL{ndorel:1}{\NDA{A \vee B}}
+        {\prfsummary{\NDDL{ndorel:1}{A}}{C}}
+        {\prfsummary{\NDDL{[l]ndorel:1}{B}}{C}}{C}} \quad
+      \vcenter{\NDORE{\NDA{A \vee B}}{\prfsummary{\NDA{A}}{C}}
+        {\prfsummary{\NDA{B}}{C}}{C}}\enspace;
+    \end{prfenv}
+  \end{displaymath}
+\item \verb|\NDIMPIL|, \verb|\NDIMPI|: implication introduction,
+  possibly labelled
+  \begin{displaymath}
+    \begin{prfenv}
+      \vcenter{\NDIMPIL{ndimpil:1}
+        {\prfsummary{\NDDL{ndimpil:1}{A}}{B}}
+        {A \rightarrow B}} \quad
+      \vcenter{\NDIMPI{\prfsummary{\NDA{A}}{B}}{A \rightarrow B}}
+      \enspace;
+    \end{prfenv}
+  \end{displaymath}
+\item \verb|\NDIMPE|: implication elimination
+  \begin{displaymath}
+    \begin{prfenv}
+      \vcenter{\NDIMPE{\NDA{A \rightarrow B}}{\NDA{A}}{B}}\enspace; 
+    \end{prfenv}
+  \end{displaymath}
+\item \verb|\NDNOTIL|, \verb|\NDNOTI|: negation introduction, possibly
+  labelled
+  \begin{displaymath}
+    \begin{prfenv}
+      \vcenter{\NDNOTIL{ndnotil:1}
+        {\prfsummary{\NDDL{ndnotil:1}{A}}{\bot}}{\neg A}}\quad
+      \vcenter{\NDNOTI{\prfsummary{\NDA{A}}{\bot}}{\neg A}}\enspace; 
+    \end{prfenv}
+  \end{displaymath}
+\item \verb|\NDNOTE|: negation elimination
+  \begin{displaymath}
+    \begin{prfenv}
+      \vcenter{\NDNOTE{\NDA{\neg A}}{\NDA{A}}{\bot}}\enspace;
+    \end{prfenv}
+  \end{displaymath}
+\item \verb|\NDALLI|: universal quantifier introduction
+  \begin{displaymath}
+    \begin{prfenv}
+      \vcenter{\NDALLI{\NDA{A}}{\forall x.\, A}}\enspace;
+    \end{prfenv}
+  \end{displaymath}
+\item \verb|\NDALLE|: universal quantifier elimination
+  \begin{displaymath}
+    \begin{prfenv}
+      \vcenter{\NDALLE{\NDA{\forall x.\, A}}{A[t/x]}}\enspace;
+    \end{prfenv}
+  \end{displaymath}
+\item \verb|\NDEXI|: existential quantifier introduction
+  \begin{displaymath}
+    \begin{prfenv}
+      \vcenter{\NDEXI{\NDA{A[t/x]}}{\exists x.\, A}}\enspace; 
+    \end{prfenv}
+  \end{displaymath}
+\item \verb|\NDEXEL|, \verb|\NDEXE|: existential quantifier
+  elimination, possibly labelled
+  \begin{displaymath}
+    \begin{prfenv}
+      \vcenter{\NDEXEL{ndexel:1}{\NDA{\exists x.\, A}}
+        {\prfsummary{\NDDL{ndexel:1}{A}}{B}}{B}}\quad
+      \vcenter{\NDEXE{\NDA{\exists x.\, A}}
+        {\prfsummary{\NDA{A}}{B}}{B}}\enspace;
+    \end{prfenv}
+  \end{displaymath}
+\item \verb|\NDTI|: truth introduction
+  \begin{displaymath}
+    \begin{prfenv}
+      \vcenter{\NDTI{\top}}\enspace;
+    \end{prfenv}
+  \end{displaymath}
+\item \verb|\NDFE|: falsity elimination
+  \begin{displaymath}
+    \begin{prfenv}
+      \vcenter{\NDFE{\NDA{\bot}}{A}}\enspace;
+    \end{prfenv}
+  \end{displaymath}
+\item \verb|\NDLEM|: law of Excluded Middle
+  \begin{displaymath}
+    \begin{prfenv}
+      \vcenter{\NDLEM{A \vee \neg A}}\enspace.
+    \end{prfenv}
+  \end{displaymath}
 \end{itemize}
 
 The labels, when present, are the first argument, the rest being the
@@ -1033,36 +1126,127 @@ is typeset in abbreviated form by the following code
     {\neg\neg A \supset A}
 \end{verbatim}\vspace{2ex}
 
-Similarly, by loading the package as
-\verb|\usepackage[SEQ]{prftree.sty}|, the following abbreviations
-are available, which roughly correspond to the inference rule of
-sequent calculi:
+\subsection{Sequents}
+Similarly, by loading the package with the \verb|SEQ| option, the
+following abbreviations are available, which roughly correspond to the
+inference rule of sequent calculi:
 \begin{itemize}
 \item \verb|\SEQA|: assumption;
-\item \verb|\SEQD|: bounded assumption;
+\item \verb|\SEQD|: bounded assumption (not normally used, but handy
+  to have in case of fancy calculi);
 \item \verb|\SEQP|: generic proof;
-\item \verb|\SEQAX|: axiom rule;
-\item \verb|\SEQLF|: left falsity;
-\item \verb|\SEQLW|: left weakening;
-\item \verb|\SEQRW|: right weakening;
-\item \verb|\SEQLC|: left contraction;
-\item \verb|\SEQRC|: right contraction;
-\item \verb|\SEQLAND|: left conjunction;
-\item \verb|\SEQRAND|: right conjunction;
-\item \verb|\SEQLOR|: left disjunction;
-\item \verb|\SEQROR|: right disjunction;
-\item \verb|\SEQLIMP|: left implication;
-\item \verb|\SEQRIMP|: right implication;
-\item \verb|\SEQLALL|: left universal quantification;
-\item \verb|\SEQRALL|: right universal quantification;
-\item \verb|\SEQLEX|:  left existential quantification;
-\item \verb|\SEQREX|: right existential quantification;
-\item \verb|\SEQCUT|: cut rule.
+\item \verb|\SEQAX|: axiom rule
+  \begin{displaymath}
+    \vcenter{\SEQAX{A \Rightarrow A}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQLF|: left falsity
+  \begin{displaymath}
+    \vcenter{\SEQLF{\bot \Rightarrow {}}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQLW|, \verb|\SEQRW|: left and right weakening
+  \begin{displaymath}
+    \vcenter{\SEQLW{\Gamma \Rightarrow \Delta}{A, \Gamma \Rightarrow
+      \Delta}}\quad 
+    \vcenter{\SEQLW{\Gamma \Rightarrow \Delta}{\Gamma \Rightarrow
+      \Delta, A}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQLC|, \verb|\SEQRC|: left and right contraction
+  \begin{displaymath}
+    \vcenter{\SEQLC{A, A, \Gamma \Rightarrow \Delta}{A, \Gamma
+        \Rightarrow \Delta}}\quad
+    \vcenter{\SEQRC{\Gamma \Rightarrow \Delta, A, A}{\Gamma
+        \Rightarrow \Delta, A}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQLAND|, \verb|\SEQLANDL|, \verb|\SEQLANDR|: left
+  conjunction; the \verb|L| and \verb|R| variants specify which side
+  of the conjunction is introduced
+  \begin{displaymath}
+    \vcenter{\SEQLANDL{A, \Gamma \Rightarrow \Delta}{A \wedge B, \Gamma
+      \Rightarrow \Delta}}\quad
+    \vcenter{\SEQLANDR{B, \Gamma \Rightarrow \Delta}{A \wedge B, \Gamma
+      \Rightarrow \Delta}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQRAND|: right conjunction
+  \begin{displaymath}
+    \vcenter{\SEQRAND{\Gamma \Rightarrow \Delta, A}{\Gamma \Rightarrow
+      \Delta, B}{\Gamma \Rightarrow \Delta, A \wedge B}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQLOR|: left disjunction
+  \begin{displaymath}
+    \vcenter{\SEQLOR{A, \Gamma \Rightarrow \Delta}{B, \Gamma
+        \Rightarrow \Delta}{A \vee B, \Gamma \Rightarrow
+        \Delta}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQROR|, \verb|\SEQRORL|, \verb|\SEQRORR|: right
+  disjunction; the \verb|R| and \verb|L| variants specify which side
+  of the disjunction is introduced
+  \begin{displaymath}
+    \vcenter{\SEQRORL{\Gamma \Rightarrow \Delta, A}{\Gamma \Rightarrow
+        \Delta, A \vee B}}\quad
+    \vcenter{\SEQRORR{\Gamma \Rightarrow \Delta, B}{\Gamma \Rightarrow
+        \Delta, A \vee B}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQLIMP|: left implication
+  \begin{displaymath}
+    \vcenter{\SEQLIMP{\Gamma \Rightarrow \Delta, A}{B, \Gamma
+        \Rightarrow \Delta}{A \rightarrow B, \Gamma \Rightarrow
+        \Delta}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQRIMP|: right implication
+  \begin{displaymath}
+    \vcenter{\SEQRIMP{A, \Gamma \Rightarrow \Delta, B}{\Gamma
+        \Rightarrow, \Delta, A \rightarrow B}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQLALL|: left universal quantification
+  \begin{displaymath}
+    \vcenter{\SEQLALL{A[t/x], \Gamma \Rightarrow \Delta}{\forall x.\,
+        A, \Gamma \Rightarrow \Delta}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQRALL|: right universal quantification
+  \begin{displaymath}
+    \vcenter{\SEQRALL{\Gamma \Rightarrow \Delta, A}{\Gamma \Rightarrow
+      \Delta, \forall x.\, A}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQLEX|:  left existential quantification
+  \begin{displaymath}
+    \vcenter{\SEQLEX{A, \Gamma \Rightarrow \Delta}{\exists x.\, A,
+        \Gamma \Rightarrow \Delta}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQREX|: right existential quantification
+  \begin{displaymath}
+    \vcenter{\SEQREX{\Gamma \Rightarrow \Delta, A[t/x]}{\Gamma
+        \Rightarrow \Delta, \exists x.\, A}}\enspace;
+  \end{displaymath}
+\item \verb|\SEQCUT|: cut rule
+  \begin{displaymath}
+    \vcenter{\SEQCUT{\Gamma \Rightarrow \Delta, A}{A, \Gamma'
+        \Rightarrow \Delta'}{\Gamma \Gamma' \Rightarrow \Delta
+        \Delta'}}\enspace.
+  \end{displaymath}
 \end{itemize}
 
-One can load the package with both options at the same
-time.\vspace{2ex}
+\subsection{Equality}
+Invoking the \verb|EQ| option defines the following inference rules:
+\begin{itemize}
+\item \verb|\EQREFL|: reflexivity
+  \begin{displaymath}
+    \vcenter{\EQREFL{t = t}}\enspace;
+  \end{displaymath}
+\item \verb|\EQSYM|: symmetry
+  \begin{displaymath}
+    \vcenter{\EQSYM{t = s}{s = t}}\enspace;
+  \end{displaymath}
+\item \verb|\EQTRANS|: transitivity
+  \begin{displaymath}
+    \vcenter{\EQTRANS{t = s}{s = r}{t = r}}\enspace;
+  \end{displaymath}
+\item \verb|\EQSUBST|: the substitution rule
+  \begin{displaymath}
+    \vcenter{\EQSUBST{t = s}{A[t/x]}{A[s/x]}}\enspace.
+  \end{displaymath}
+\end{itemize}
 
+\subsection{Implication}
 Since the implication symbol is usually represented either as
 $\rightarrow$ or as $\supset$, the package allows to choose which
 representation to use. By default, implication is $\rightarrow$, but
@@ -1071,10 +1255,402 @@ $\supset$. The same effect is obtained by the commands
 \verb|\prfIMPOptiontrue| (implication is $\supset$) and
 \verb|prfIMPOptionfalse| (implication is $\rightarrow$).
 
+\subsection{Martin-L{\"o}f Type Theory and Homotopy Type Theory}
+Invoking the package with the \verb|ML| option enables the support for
+these type theories. This part is derived from Roberta Bonacina's PhD
+dissertation, which used this package in an essential way to develop
+proof trees in Homotopy Type Theory.
+
+Enabling the option \verb|ML| defines a number of symbols which are
+useful to have. However, since they may conflict with other packages,
+they can be disabled invoking the option \verb|MLnodef|. These
+operators are
+\begin{itemize}
+\item \verb|\type|: the symbol $\type$ correctly spaced as a
+  mathematical binary operation;
+\item \verb|\universe|: the symbol for universes;
+\item \verb|\judgementaldef| and \verb|\propositionaldef|: the symbols
+  $\judgementaldef$ and $\propositionaldef$ spaced as mathematical
+  binary operations;
+\item \verb|\emptytype| ($\emptytype$), \verb|\unittype|
+  ($\unittype$), \verb|\booleantype| ($\booleantype$): these symbols
+  are ordinary operators typeset in mathematical boldface font;
+\item \verb|\context| ($\context$), \verb|\identitytype|
+  ($\identitytype$), \verb|\refl| ($\refl$), \verb|\axiomofchoice|
+  ($\axiomofchoice$), \verb|\accessibility| ($\accessibility$),
+  \verb|\ap| ($\ap$), \verb|\apd| ($\apd$), \verb|\basepoint|
+  ($\basepoint$), \verb|\biinv| ($\biinv$), \verb|\cardtype|
+  ($\cardtype$), \verb|\cocone| ($\cocone$), \verb|\cons| ($\cons$),
+  \verb|\contr| ($\contr$), \verb|\equivtype| ($\equivtype$),
+  \verb|\ext| ($\ext$), \verb|\fiber| ($\fiber$), \verb|\funext|
+  ($\funext$), \verb|\glue| ($\glue$), \verb|\happly| ($\happly$),
+  \verb|\hom| ($\hom$), \verb|\id| ($\id$), \verb|\idtoeqv|
+  ($\idtoeqv$), \verb|\im| ($\im$), \verb|\idtoiso| ($\idtoiso$),
+  \verb|\ind| ($\ind$), \verb|\inj| ($\inj$), \verb|\inl| ($\inl$),
+  \verb|\inr| ($\inr$), \verb|\iscontr| ($\iscontr$), \verb|\isequiv|
+  ($\isequiv$), \verb|\ishae| ($\ishae$), \verb|\isotoid|
+  ($\isotoid$), \verb|\isprop| ($\isprop$), \verb|\isset| ($\isset$),
+  \verb|\ker| ($\ker$), \verb|\LEM| ($\LEM$), \verb|\linv| ($\linv$),
+  \verb|\listtype| ($\listtype$), \verb|\loopcons| ($\loopcons$),
+  \verb|\Map| ($\Map$), \verb|\merid| ($\merid$), \verb|\nil|
+  ($\nil$), \verb|\ordtype| ($\ordtype$), \verb|\pair| ($\pair$),
+  \verb|\pred| ($\pred$), \verb|\pr| ($\pr$), \verb|\Prop| ($\Prop$),
+  \verb|\qinv| ($\qinv$), \verb|\rec| ($\rec$), \verb|\rinv|
+  ($\rinv$), \verb|\seg| ($\seg$), \verb|\Set| ($\Set$), \verb|\Succ|
+  ($\Succ$), \verb|\sup| ($\sup$), \verb|\total| ($\total$),
+  \verb|\transport| ($\transport$), \verb|\ua| ($\ua$), \verb|\Wtype|
+  ($\Wtype$), \verb|\transportconst| ($\transportconst$): these
+  symbols are ordinary operators, typeset in the mathematical
+  sans-serif font; their graphical appearance is in brackets.
+\end{itemize}
+
+The large number of inference rules is listed below: they cover the
+structural part of the theories, plus most of the usual inductive
+types, comprehending also some higher-order inductive types. To each
+rule is associated a rule name, which is available as a command: the
+convention is that the rule name is obtained appending \verb|rule| to
+the name of the inference rule. In general, the command to typeset a
+rule conforms to the standard name in the book \emph{Homotopy Type
+  Theory}. The name as typeset, is shown in brackets:
+\begin{itemize}
+\item \verb|\MLctxEMP| $(\scriptstyle\MLctxEMPrule)$,\\ \verb|\MLctxEXT|
+  $(\scriptstyle\MLctxEXTrule)$: context manipulation;
+\item \verb|\MLVble| $(\scriptstyle\MLVblerule)$: variable
+  introduction;
+\item \verb|\MLSubst| $(\scriptstyle\MLSubstrule)$, 
+  \verb|\MLWkg|
+  $(\scriptstyle\MLWkgrule)$: substitution and weakening;
+\item \verb|\MLEQrefl| $(\scriptstyle\MLEQreflrule)$,
+  \verb|\MLEQsym| $(\scriptstyle\MLEQsymrule)$, 
+  \verb|\MLEQtrans| $(\scriptstyle\MLEQtransrule)$, \\
+  \verb|\MLEQsubst| $(\scriptstyle\MLEQsubstrule)$, 
+  \verb|\MLEQsubsteq| $(\scriptstyle\MLEQsubsteqrule)$: structural
+  rules about judgemental equality;
+\item \verb|\MLUintro| $(\scriptstyle\MLUintrorule)$, 
+  \verb|\MLUcumul| $(\scriptstyle\MLUcumulrule)$, 
+  \verb|\MLUcumuleq| $(\scriptstyle\MLUcumuleqrule)$: type universe;
+\item \verb|\MLpiform| $(\scriptstyle\MLpiformrule)$, 
+  \verb|\MLpiformeq| $(\scriptstyle\MLpiformeqrule)$, \\
+  \verb|\MLpiintro| $(\scriptstyle\MLpiintrorule)$, 
+  \verb|\MLpiintroeq| $(\scriptstyle\MLpiintroeqrule)$, \\
+  \verb|\MLpielim| $(\scriptstyle\MLpielimrule)$, 
+  \verb|\MLpielimeq| $(\scriptstyle\MLpielimeqrule)$, \\
+  \verb|\MLpicomp| $(\scriptstyle\MLpicomprule)$, 
+  \verb|\MLpiuniq| $(\scriptstyle\MLpiuniqrule)$: dependent function
+  types;
+\item \verb|\MLKintro| $(\scriptstyle\MLKintrorule)$: generic rule for
+  constant introduction;
+\item \verb|\MLsigmaform| $(\scriptstyle\MLsigmaformrule)$, 
+  \verb|\MLsigmaintro| $(\scriptstyle\MLsigmaintrorule)$, 
+  \verb|\MLsigmaelim| $(\scriptstyle\MLsigmaelimrule)$, \\
+  \verb|\MLsigmacomp| $(\scriptstyle\MLsigmacomprule)$, 
+  \verb|\MLsigmauniq| $(\scriptstyle\MLsigmauniqrule)$: dependent pair
+  types;
+\item \verb|\MLplusform| $(\scriptstyle\MLplusformrule)$, 
+  \verb|\MLplusintrol| $(\scriptstyle\MLplusintrolrule)$, 
+  \verb|\MLplusintror| $(\scriptstyle\MLplusintrorrule)$, \\
+  \verb|\MLpluselim| $(\scriptstyle\MLpluselimrule)$, 
+  \verb|\MLpluscompl| $(\scriptstyle\MLpluscomplrule)$, 
+  \verb|\MLpluscompr| $(\scriptstyle\MLpluscomprrule)$, \\ 
+  \verb|\MLplusuniq| $(\scriptstyle\MLplusuniqrule)$: coproduct types;
+\item \verb|\MLzeroform| $(\scriptstyle\MLzeroformrule)$, 
+  \verb|\MLzeroelim| $(\scriptstyle\MLzeroelimrule)$, 
+  \verb|\MLzerouniq| $(\scriptstyle\MLzerouniqrule)$: the empty type;
+\item \verb|\MLunitform| $(\scriptstyle\MLunitformrule)$, 
+  \verb|\MLunitintro| $(\scriptstyle\MLunitintrorule)$, 
+  \verb|\MLunitelim| $(\scriptstyle\MLunitelimrule)$, \\
+  \verb|\MLunitcomp| $(\scriptstyle\MLunitcomprule)$, 
+  \verb|\MLunituniq| $(\scriptstyle\MLunituniqrule)$: the unit type;
+\item \verb|\MLnatform| $(\scriptstyle\MLnatformrule)$, 
+  \verb|\MLnatintrozero| $(\scriptstyle\MLnatintrozerorule)$, \\
+  \verb|\MLnatintrosucc| $(\scriptstyle\MLnatintrosuccrule)$, 
+  \verb|\MLnatelim| $(\scriptstyle\MLnatelimrule)$, \\
+  \verb|\MLnatcompzero| $(\scriptstyle\MLnatcompzerorule)$, 
+  \verb|\MLnatcompsucc| $(\scriptstyle\MLnatcompsuccrule)$, \\
+  \verb|\MLnatuniq| $(\scriptstyle\MLnatuniqrule)$: the natural number
+  type;
+\item \verb|\MLidform| $(\scriptstyle\MLidformrule)$,
+  \verb|\MLidintro| $(\scriptstyle\MLidintrorule)$,
+  \verb|\MLidelim| $(\scriptstyle\MLidelimrule)$, \\
+  \verb|\MLidcomp| $(\scriptstyle\MLidcomprule)$,
+  \verb|\MLiduniq| $(\scriptstyle\MLiduniqrule)$: identity types;
+\item \verb|\MLwform| $(\scriptstyle\MLwformrule)$,
+  \verb|\MLwintro| $(\scriptstyle\MLwintrorule)$,
+  \verb|\MLwelim| $(\scriptstyle\MLwelimrule)$, \\
+  \verb|\MLwcomp| $(\scriptstyle\MLwcomprule)$,
+  \verb|\MLwuniq| $(\scriptstyle\MLwuniqrule)$: $\mathsf{W}$ types;
+\item \verb|\MLListform| $(\scriptstyle\MLListformrule)$,
+  \verb|\MLListintron| $(\scriptstyle\MLListintronrule)$,\\
+  \verb|\MLListintroc| $(\scriptstyle\MLListintrocrule)$,
+  \verb|\MLListelim| $(\scriptstyle\MLListelimrule)$,\\
+  \verb|\MLListcompn| $(\scriptstyle\MLListcompnrule)$,
+  \verb|\MLListcompc| $(\scriptstyle\MLListcompcrule)$,\\
+  \verb|\MLListuniq| $(\scriptstyle\MLListuniqrule)$:
+  $\mathsf{List}$ types;
+\item \verb|\MLfunext| $(\scriptstyle\MLfunextrule)$: function extensionality;
+\item \verb|\MLuniv| $(\scriptstyle\MLunivrule)$: univalence;
+\item \verb|\MLSform| $(\scriptstyle\MLSformrule)$,
+  \verb|\MLSintro| $(\scriptstyle\MLSintrorule)$,
+  \verb|\MLSelim| $(\scriptstyle\MLSelimrule)$,\\
+  \verb|\MLScomp| $(\scriptstyle\MLScomprule)$,
+  \verb|\MLSuniq| $(\scriptstyle\MLSuniqrule)$,
+  \verb|\MLSpeqintro| $(\scriptstyle\MLSpeqintrorule)$,\\
+  \verb|\MLSpeqcomp| $(\scriptstyle\MLSpeqcomprule)$: the
+  $\mathbb{S}^1$ circle type;
+\item \verb|\MLIform| $(\scriptstyle\MLIformrule)$,
+  \verb|\MLIintroa| $(\scriptstyle\MLIintroarule)$,
+  \verb|\MLIintrob| $(\scriptstyle\MLIintrobrule)$, \\
+  \verb|\MLIelim| $(\scriptstyle\MLIelimrule)$,
+  \verb|\MLIcompa| $(\scriptstyle\MLIcomparule)$,
+  \verb|\MLIcompb| $(\scriptstyle\MLIcompbrule)$, \\
+  \verb|\MLIuniq| $(\scriptstyle\MLIuniqrule)$,
+  \verb|\MLIpeqintro| $(\scriptstyle\MLIpeqintrorule)$,
+  \verb|\MLIpeqcomp| $(\scriptstyle\MLIpeqcomprule)$: the interval
+  type; 
+\item \verb|\MLsigmaintroa| $(\scriptstyle\MLsigmaintroarule)$,
+  \verb|\MLsigmaintrob| $(\scriptstyle\MLsigmaintrobrule)$, \\
+  \verb|\MLsigmacompa| $(\scriptstyle\MLsigmacomparule)$,
+  \verb|\MLsigmacompb| $(\scriptstyle\MLsigmacompbrule)$, \\
+  \verb|\MLsigmapeqintro| $(\scriptstyle\MLsigmapeqintrorule)$,
+  \verb|\MLsigmapeqcomp| $(\scriptstyle\MLsigmapeqcomprule)$:
+  suspensions;
+\item \verb|\MLPOform| $(\scriptstyle\MLPOformrule)$,
+  \verb|\MLPOintroa| $(\scriptstyle\MLPOintroarule)$,
+  \verb|\MLPOintrob| $(\scriptstyle\MLPOintrobrule)$, \\
+  \verb|\MLPOelim| $(\scriptstyle\MLPOelimrule)$,
+  \verb|\MLPOcompa| $(\scriptstyle\MLPOcomparule)$,
+  \verb|\MLPOcompb| $(\scriptstyle\MLPOcompbrule)$, \\
+  \verb|\MLPOuniq| $(\scriptstyle\MLPOuniqrule)$,
+  \verb|\MLPOpeqintro| $(\scriptstyle\MLPOpeqintrorule)$,
+  \verb|\MLPOpeqcomp| $(\scriptstyle\MLPOpeqcomprule)$: pushouts;
+\item \verb|\MLTform| $(\scriptstyle\MLTformrule)$,
+  \verb|\MLTintro| $(\scriptstyle\MLTintrorule)$,
+  \verb|\MLTelim| $(\scriptstyle\MLTelimrule)$, \\
+  \verb|\MLTcomp| $(\scriptstyle\MLTcomprule)$,
+  \verb|\MLTuniq| $(\scriptstyle\MLTuniqrule)$,
+  \verb|\MLTpeqintro| $(\scriptstyle\MLTpeqintrorule)$, \\
+  \verb|\MLTpeqcomp| $(\scriptstyle\MLTpeqcomprule)$: truncations;
+\item \verb|\MLtorusform| $(\scriptstyle\MLtorusformrule)$,
+  \verb|\MLtorusintro| $(\scriptstyle\MLtorusintrorule)$,
+  \verb|\MLtoruselim| $(\scriptstyle\MLtoruselimrule)$,\\
+  \verb|\MLtoruscomp| $(\scriptstyle\MLtoruscomprule)$,
+  \verb|\MLtoruspeqintroa| $(\scriptstyle\MLtoruspeqintroarule)$, \\
+  \verb|\MLtoruspeqintrob| $(\scriptstyle\MLtoruspeqintrobrule)$,
+  \verb|\MLtoruspeqintroc| $(\scriptstyle\MLtoruspeqintrocrule)$, \\
+  \verb|\MLtoruspeqcompa| $(\scriptstyle\MLtoruspeqcomparule)$,
+  \verb|\MLtoruspeqcompb| $(\scriptstyle\MLtoruspeqcompbrule)$, \\
+  \verb|\MLtoruspeqcompc| $(\scriptstyle\MLtoruspeqcompcrule)$:
+  the torus type.
+\end{itemize}
+
+\subsection{Defining new inference rules}
 Of course, the reader is encouraged to develop her own abbreviations
-starting from the provided ones.
+starting from the provided ones. To this aim two commands are
+provided. They share the same syntax: \verb|\prfMakeInferenceRule| and
+\verb|\prfMakeInferenceRuleRef| take two arguments, the first one is
+the name of the command associated to the inference rule, and the
+second one is used to write the rule name. For example,
+\begin{center}
+  \verb|\prfMakeInferenceRule{NDANDI}{\mathord{\wedge}\textup{I}}| 
+\end{center}
+is how the conjunction introduction rule is defined, and
+\begin{center}
+  \verb|  \prfMakeInferenceRuleRef{NDOREL}{\mathord{\vee}\textup{E}}|
+\end{center}
+is how the disjunction elimination rule is defined. The rules
+generated by the \verb|Ref| variant use their first argument as the
+reference to the assumption(s) they discharge.
+
+\subsection{Stacking proofs and assumptions}
+Sometimes, a proof is too large to fit into the text width. Although
+some strategies could be implemented to compress it, see the next
+section, they fail in extreme cases. For example, the elimination rule
+for the circle in Homotopy type theories is:
+\begin{displaymath}
+  \MLScomp
+  {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i}
+  {\Gamma \vdash b \type C[\basepoint/x]}
+  {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b}
+  {\Gamma \vdash p \type \mathbb{S}^1}
+  {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+    \type C[p/x]}
+\end{displaymath}
+typeset by
+\begin{verbatim}
+  \MLScomp
+  {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i}
+  {\Gamma \vdash b \type C[\basepoint/x]}
+  {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b}
+  {\Gamma \vdash p \type \mathbb{S}^1}
+  {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+    \type C[p/x]}
+\end{verbatim}
+It is clear that on an A5 paper, there is not enough space to write it
+down. In these cases, the package provides a way to \emph{stack} the
+premises of a rule, obtaining
+\begin{displaymath}
+  \MLScomp
+  {\prfStackPremises
+    {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i}
+    {\Gamma \vdash b \type C[\basepoint/x]} }
+  {\prfStackPremises
+    {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b}
+    {\Gamma \vdash p \type \mathbb{S}^1} }
+  {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+    \type C[p/x]}
+\end{displaymath}
+The corresponding \LaTeX{} code is
+\begin{verbatim}
+  \MLScomp
+  {\prfStackPremises
+    {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i}
+    {\Gamma \vdash b \type C[\basepoint/x]} 
+  }
+  {\prfStackPremises
+    {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b}
+    {\Gamma \vdash p \type \mathbb{S}^1} 
+  }
+  {\Gamma \vdash 
+    \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) \type C[p/x]}
+\end{verbatim}
+The command
+\verb|\prfStackPremises{|$a_1$\verb|}{|$\ldots$\verb|}{|$a_n$\verb|}|
+takes the arguments $a_1, \ldots, a_n$ and typeset them as a proof
+tree with no lines with $a_1$ on the top.
 
-% -------------------------------------
+Actually, stacking proofs is possible:
+\begin{displaymath}
+  \MLScomp
+  {\prfStackPremises
+    {\prfsummary{\Gamma\;\context}
+      {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type
+        \universe_i}} 
+    {\prfsummary{\Gamma\;\context}
+      {\Gamma \vdash \basepoint \type \mathbb{S}^1}} }
+  {\prfStackPremises
+    {\prfsummary{\Gamma\;\context}
+      {\Gamma \vdash \ell \type \basepoint = \basepoint}}
+    {\prfsummary{\Gamma\;\context}
+      {\Gamma \vdash p \type \mathbb{S}^1}} }
+  {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+    \type C[p/x]}
+\end{displaymath}
+has been typeset by
+\begin{verbatim}
+  \MLScomp
+  {\prfStackPremises
+    {\prfsummary{\Gamma\;\context}
+      {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type
+        \universe_i}} 
+    {\prfsummary{\Gamma\;\context}
+      {\Gamma \vdash \basepoint \type \mathbb{S}^1}} 
+  }
+  {\prfStackPremises
+    {\prfsummary{\Gamma\;\context}
+      {\Gamma \vdash \ell \type \basepoint = \basepoint}}
+    {\prfsummary{\Gamma\;\context}
+      {\Gamma \vdash p \type \mathbb{S}^1}} 
+  }
+  {\Gamma \vdash 
+     \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) \type C[p/x]}
+\end{verbatim}
+
+Since a stack is a proof tree, the parameters could be locally changed
+to control its appearance. For example
+\begin{displaymath}
+  \MLScomp
+  {\prfemptylinethickness20\prflinethickness
+    \prfStackPremises
+    {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i}
+    {\Gamma \vdash b \type C[\basepoint/x]} }
+  {\prfStackPremises
+    {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b}
+    {\Gamma \vdash p \type \mathbb{S}^1} }
+  {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+    \type C[p/x]}
+\end{displaymath}
+makes the lines in the left stack far apart. 
+\begin{verbatim}
+  \MLScomp
+  {\prfemptylinethickness20\prflinethickness
+    \prfStackPremises
+    {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i}
+    {\Gamma \vdash b \type C[\basepoint/x]} }
+  {\prfStackPremises
+    {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b}
+    {\Gamma \vdash p \type \mathbb{S}^1} }
+  {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+    \type C[p/x]}
+\end{verbatim}
+
+Spacing in stacks of proofs is normally difficult to control: if
+really sophisticated formatting is needed, it is better to consider
+the following option:
+\begin{displaymath}
+  \MLScomp
+  {\prfassumption{
+      \begin{array}{@{}c@{\quad}c@{}}
+        {\prfsummary{\Gamma\;\context}
+          {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type
+            \universe_i}} &
+        {\Gamma \vdash \ell \type \basepoint = \basepoint} \\
+        {\prfsummary{\Gamma\;\context}
+          {\Gamma \vdash \basepoint \type \mathbb{S}^1}} &
+        {\Gamma \vdash p \type \mathbb{S}^1}
+      \end{array}}}
+  {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+    \type C[p/x]}
+\end{displaymath}
+which uses the \verb|array| environment
+\begin{verbatim}
+  \MLScomp
+  {\prfassumption{
+      \begin{array}{@{}c@{\quad}c@{}}
+        {\prfsummary{\Gamma\;\context}
+          {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type
+            \universe_i}} &
+        {\Gamma \vdash \ell \type \basepoint = \basepoint} \\
+        {\prfsummary{\Gamma\;\context}
+          {\Gamma \vdash \basepoint \type \mathbb{S}^1}} &
+        {\Gamma \vdash p \type \mathbb{S}^1}
+      \end{array}}}
+  {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+    \type C[p/x]}
+\end{verbatim}
+or similar ones, using the multitude of packages to format tables. By
+the way, the obvious solution using stacks is
+\begin{displaymath}
+  \MLScomp
+  {\prfStackPremises
+    {\prfsummary{\Gamma\;\context}
+      {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type
+        \universe_i}} 
+    {\prfsummary{\Gamma\;\context}
+      {\Gamma \vdash \basepoint \type \mathbb{S}^1}} }
+  {\prfStackPremises
+    {\prfassumption
+      {\Gamma \vdash \ell \type \basepoint = \basepoint}}
+    {\prfassumption
+      {\Gamma \vdash p \type \mathbb{S}^1}} }
+  {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+    \type C[p/x]}
+\end{displaymath}
+\begin{verbatim}
+  \MLScomp
+  {\prfStackPremises{\prfsummary{\Gamma\;\context}
+      {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type
+        \universe_i}} 
+    {\prfsummary{\Gamma\;\context}
+      {\Gamma \vdash \basepoint \type \mathbb{S}^1}} }
+  {\prfStackPremises{\prfassumption
+      {\Gamma \vdash \ell \type \basepoint = \basepoint}}
+    {\prfassumption
+      {\Gamma \vdash p \type \mathbb{S}^1}} }
+  {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+    \type C[p/x]}
+\end{verbatim}
+
+%-------------------------------------
 \clearpage
 \section{Hints and Tricks}\label{sec:hints_and_tricks}
 This section shows a few hints and tricks to use the package at its
@@ -1202,8 +1778,9 @@ is slightly better to vertically centre the box, as in
 \end{verbatim}
 
 Of course, the result is not pleasant, because rows are far apart,
-which is unavoidable because of the height of the proof tree.  The
-same principle applies also to arrays of proof trees:
+which is unavoidable because of the height of the proof tree.
+
+The same principle applies also to arrays of proof trees:
 \begin{displaymath}
   \begin{array}{lcccc}
     \text{some text} &
@@ -1219,6 +1796,7 @@ same principle applies also to arrays of proof trees:
     \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}}
   \end{array}
 \end{displaymath}
+which has been typeset by
 \begin{verbatim}
   \begin{array}{lcccc}
     \text{some text} &
@@ -1284,21 +1862,21 @@ we may consider to define
   \setcounter{prfsummarycounter}{0}
   \setcounter{prfassumptioncounter}{0}
   \mbox{Let }
-  \vcenter{\prfsummary<[f]s:abbrev>
+  \left(\vcenter{\prfsummary<[f]s:abbrev>
       {\NDDL{s:notnotA}{\neg\neg A}}
       {\NDAL{s:notA}{\neg A}}
-      {\neg\neg A \supset A}}
+      {\neg\neg A \supset A}}\right)
   \equiv
-  \vcenter{\NDIMPIL{s:notnotA}
+  \left(\vcenter{\NDIMPIL{s:notnotA}
       {\NDFE{\NDIMPE{\NDDL{[l]s:notnotA}{\neg\neg A}}
           {\NDAL{[l]s:notA}{\neg A}}{\bot}}{A}} 
-      {\neg\neg A \supset A}}
+      {\neg\neg A \supset A}}\right)
 \end{displaymath}
 allowing to abbreviate the whole proof as
 \begin{displaymath}
   \NDOREL{s:notA}{\NDLEM{A \vee \neg A}}
   {\NDIMPI{\NDDL{[l]s:notA}{A}}{\neg\neg A \supset A}}
-  {\prfsummary<s:abbrev>
+  {\hspace{-1em}\prfsummary<s:abbrev>
     {\NDDL{[l]s:notnotA}{\neg\neg A}}
     {\NDDL{[l]s:notA}{\neg A}}
       {\neg\neg A \supset A}}
@@ -1310,21 +1888,21 @@ The corresponding \LaTeX{} code is
   \setcounter{prfsummarycounter}{0}
   \setcounter{prfassumptioncounter}{0}
   \mbox{Let }
-  \vcenter{\prfsummary<[f]s:abbrev>
+  \left(\vcenter{\prfsummary<[f]s:abbrev>
       {\NDDL{s:notnotA}{\neg\neg A}}
       {\NDAL{s:notA}{\neg A}}
-      {\neg\neg A \supset A}}
+      {\neg\neg A \supset A}}\right)
   \equiv
-  \vcenter{\NDIMPIL{s:notnotA}
+  \left(\vcenter{\NDIMPIL{s:notnotA}
       {\NDFE{\NDIMPE{\NDDL{[l]s:notnotA}{\neg\neg A}}
           {\NDAL{[l]s:notA}{\neg A}}{\bot}}{A}} 
-      {\neg\neg A \supset A}}
+      {\neg\neg A \supset A}}\right)
 \end{verbatim}
 for the definition of the proof summary, and
 \begin{verbatim}
   \NDOREL{s:notA}{\NDLEM{A \vee \neg A}}
   {\NDIMPI{\NDDL{[l]s:notA}{A}}{\neg\neg A \supset A}}
-  {\prfsummary<[l]s:abbrev>
+  {\hspace{-1em}\prfsummary<s:abbrev>
     {\NDDL{[l]s:notnotA}{\neg\neg A}}
     {\NDDL{[l]s:notA}{\neg A}}
       {\neg\neg A \supset A}}
@@ -1467,37 +2045,39 @@ The disjunction elimination rule, with various line options:
 
 Proof that the Law of Excluded middle implies $\neg\neg A \supset A$:
 \begin{displaymath}
-  \prftree[r]{$\vee$E}
-  {\prfbyaxiom{LEM}
+  \prfIMPOptiontrue
+  \NDORE
+  {\NDLEM
     {A \vee \neg A}\hspace{.4em}}
-  {\prftree[r]{$\supset$I}
-    {\prfboundedassumption{A}}
+  {\NDIMPI
+    {\NDD{A}}
     {\neg\neg A \supset A}}
-  {\prftree[r]{$\supset$I}
-    {\prftree[r]{$\bot$E}
-      {\prftree[r]{$\supset$E}
-        {\prfboundedassumption{\neg\neg A}}
-        {\prfboundedassumption{\neg A}}
+  {\NDIMPI
+    {\NDFE
+      {\NDIMPE
+        {\NDD{\neg\neg A}}
+        {\NDD{\neg A}}
         {\bot}}
       {A}}
     {\neg\neg A \supset A}}
   {\neg\neg A \supset A}
+  \prfIMPOptionfalse
 \end{displaymath}
 
 Proof that the Law of Excluded middle implies $\neg\neg A \supset A$
 with labels instead of rule names, except on axioms:
 \begin{displaymath}
-  \prftree[l]{$\vee$E}
-  {\prfbyaxiom{LEM}
+  \prftree[l]{$\scriptstyle\vee\mathrm{E}$}
+  {\NDLEM
     {A \vee \neg A}\hspace{.6em}}
-  {\prftree[l]{$\supset$I}
-    {\prfboundedassumption{A}}
+  {\prftree[l]{$\scriptstyle\supset\mathrm{I}$}
+    {\NDD{A}}
     {\neg\neg A \supset A}}
-  {\prftree[l]{$\supset$I}
-    {\prftree[l]{$\bot$E}
-      {\prftree[l]{$\supset$E}
-        {\prfboundedassumption{\neg\neg A}}
-        {\prfboundedassumption{\neg A}}
+  {\prftree[l]{$\scriptstyle\supset\mathrm{I}$}
+    {\prftree[l]{$\scriptstyle\bot\mathrm{E}$}
+      {\prftree[l]{$\scriptstyle\supset\mathrm{E}$}
+        {\NDD{\neg\neg A}}
+        {\NDD{\neg A}}
         {\bot}}
       {A}}
     {\neg\neg A \supset A}}
@@ -1572,7 +2152,7 @@ A deduction in a sequent calculus:
     \rightarrow B) \rightarrow (A \rightarrow C))}
 \end{displaymath}
 
-Proof tree can be coloured, as kindly pointed out by Dominic Hughes:
+Proof trees can be coloured, as kindly pointed out by Dominic Hughes:
 \begin{displaymath}
   \begin{prfenv}
     \color{green}\NDIMPIL{ex6:1}
@@ -1823,12 +2403,23 @@ It is not simple to code such an algorithm in \TeX{}, but the real
 difficulty is how to represent skylines and how to store them, since
 \TeX{} provides no abstract data structures. Hence, the implementation
 of this feature has been postponed to a remote future, or to the will
-of a real \TeX{} magician.
+of a real \TeX{} magician.\vspace{2ex}
+
+The abbreviated commands reflect their use by the author. It is quite
+possible that you want to define your own commands for inference rules
+of your interest. If you think they could be of general interest, send
+them by email to the author (see below) who will include them in a
+future release of the package, acknowledging your contribution.
 \vfill
 
-Although the package has been tested for a long time, by now, it is
+Although the package has been tested for a long time by now, it is
 possible that a few bugs are still present. To signal a bug, please,
 write an email to the author (see below), possibly attaching a sample
 document which exhibit the misbehaviour, to help tracking and fixing.
 \vfill
 \end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/Master/texmf-dist/tex/latex/prftree/prftree.sty b/Master/texmf-dist/tex/latex/prftree/prftree.sty
index 8f77541c058..10d6fbce6c2 100644
--- a/Master/texmf-dist/tex/latex/prftree/prftree.sty
+++ b/Master/texmf-dist/tex/latex/prftree/prftree.sty
@@ -1,7 +1,7 @@
 %
 % prftree.sty
-% by Marco Benini - 3rd September 2016
-% v1.5
+% by Marco Benini - 19th June 2019
+% v1.6
 %
 % A package to typeset natural deduction proofs, or sequent proofs, or
 % tableau proofs
@@ -10,18 +10,25 @@
 %
 
 \NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{prftree}[2016/09/03 Natural Deduction Proofs]
+\ProvidesPackage{prftree}[2019/06/19 Natural Deduction Proofs]
 
 % Package options: deactivated by default
 \newif\ifprf@NDOption\prf@NDOptionfalse
 \newif\ifprf@SEQOption\prf@SEQOptionfalse
 \newif\ifprfIMPOption\prfIMPOptionfalse
+\newif\ifprf@EQOption\prf@EQOptionfalse
+\newif\ifprf@MLOption\prf@MLOptionfalse
+\newif\ifprf@MLnodefOption\prf@MLnodefOptionfalse
+% but the STRUT and STRUTlabel are on by default
 \newif\ifprfSTRUToption\prfSTRUToptiontrue
 \newif\ifprfSTRUTlabeloption\prfSTRUTlabeloptiontrue
 
 \DeclareOption{ND}{\prf@NDOptiontrue}
 \DeclareOption{SEQ}{\prf@SEQOptiontrue}
 \DeclareOption{IMP}{\prfIMPOptiontrue}
+\DeclareOption{EQ}{\prf@EQOptiontrue}
+\DeclareOption{ML}{\prf@MLOptiontrue}
+\DeclareOption{MLnodef}{\prf@MLnodefOptiontrue}
 \DeclareOption{Strut}{\prfSTRUToptionfalse}
 \DeclareOption{StrutLabel}{\prfSTRUTlabeloptionfalse}
 \ProcessOptions\relax
@@ -977,14 +984,42 @@
   \hbox{$\box\prf@rulenamebox$}}
 
 % -------------------------------------------------------------------
-% The following macros are used to simplify the writing of proofs in
-% natural deduction, and they roughly follow the format of proofs as
-% in Troelstra, Schwichtenberg "Basic Proof Theory".
-% 
-% Since they may conflict with other packages, they are controlled by
-% options in the package. 
+% Support macros to define new inference rules
+%
+% \prfMakeInferenceRule#1#2
+% \prfMakeInferenceRuleRef#1#2
+% #1: name of the command associated to the inference rule
+% #2: rule name
+% The plain version generates a command for typesetting a proof with
+% the inference rule; the Ref version uses the first parameter of the
+% rule as a reference that is appended to the rule name
 % -------------------------------------------------------------------
 
+\def\prfMakeInferenceRule#1#2{%
+  \expandafter\def\csname #1\endcsname%
+  {\prftree[by]{$\scriptstyle{#2}$}}}
+\def\prfMakeInferenceRuleRef#1#2{%
+  \expandafter\def\csname #1\endcsname##1%
+  {\prftree[by]{$\scriptstyle{#2}^{\prfref<##1>}$}}}
+
+% -------------------------------------------------------------------
+% Macros to stack the premises of an inference rule
+%
+% \prfStackPremises{a_1}...{a_n} generates a vertical list containing
+% a_1 on the top and a_n on the bottom.
+% -------------------------------------------------------------------
+
+\def\prfStackPremises{\prf@StackPremises{}}
+\def\prf@StackPremises#1{\@ifnextchar\bgroup%
+  {\prf@@StackPremises{\prfassumption{#1}}}%
+  {\prfassumption{#1}}}
+\def\prf@@StackPremises#1#2{\@ifnextchar\bgroup%
+  {\prf@@@StackPremises{\prftree[noline]{#1}{#2}}}%
+  {\prftree[noline]{#1}{#2}}}
+\def\prf@@@StackPremises#1#2{\@ifnextchar\bgroup%
+  {\prf@@@StackPremises{\prftree[noline]{#1}{#2}}}
+  {\prftree[noline]{#1}{#2}}}
+
 % -------------------------------------------------------------------
 % Natural deduction systems
 %
@@ -997,62 +1032,36 @@
   \def\NDAL#1{\prfassumption<#1>}
   \def\NDDL#1{\prfboundedassumption<#1>}
   \def\NDP{\prftree}
-  \def\NDANDI{\prftree[by]{$\scriptstyle\mathord{\wedge}%
-      \textup{I}$}}
-  \def\NDANDEL{\prftree[by]{$\scriptstyle\mathord{\wedge}%
-      \textup{E}_1$}}
-  \def\NDANDER{\prftree[by]{$\scriptstyle\mathord{\wedge}%
-      \textup{E}_2$}}
-  \def\NDANDE{\prftree[by]{$\scriptstyle\mathord{\wedge}%
-      \textup{E}$}}
-  \def\NDORIL{\prftree[by]{$\scriptstyle\mathord{\vee}%
-      \textup{I}_1$}}
-  \def\NDORIR{\prftree[by]{$\scriptstyle\mathord{\vee}%
-      \textup{I}_2$}}
-  \def\NDORI{\prftree[by]{$\scriptstyle\mathord{\vee}%
-      \textup{I}$}}
-  \def\NDORE{\prftree[by]{$\scriptstyle\mathord{\vee}%
-      \textup{E}$}}
-  \def\NDOREL#1{\prftree[by]{$\scriptstyle{\vee}%
-      {\textup{E}}^{\prfref<#1>}$}}
+  \prfMakeInferenceRule{NDANDI}{\mathord{\wedge}\textup{I}}
+  \prfMakeInferenceRule{NDANDEL}{\mathord{\wedge}\textup{E}_1}
+  \prfMakeInferenceRule{NDANDER}{\mathord{\wedge}\textup{E}_2}
+  \prfMakeInferenceRule{NDANDE}{\mathord{\wedge}\textup{E}}
+  \prfMakeInferenceRule{NDORIL}{\mathord{\vee}\textup{I}_1}
+  \prfMakeInferenceRule{NDORIR}{\mathord{\vee}\textup{I}_2}
+  \prfMakeInferenceRule{NDORI}{\mathord{\vee}\textup{I}}
+  \prfMakeInferenceRule{NDORE}{\mathord{\vee}\textup{E}}
+  \prfMakeInferenceRuleRef{NDOREL}{\mathord{\vee}\textup{E}}
   \ifprfIMPOption
-    \def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\supset}%
-        \textup{I}$}}
-    \def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\supset}%
-        \textup{E}$}}
-    \def\NDIMPIL#1{\prftree[by]{$\scriptstyle\mathord{\supset}%
-        \textup{I}^{\prfref<#1>}$}}
+    \prfMakeInferenceRule{NDIMPI}{\mathord{\supset}\textup{I}}
+    \prfMakeInferenceRule{NDIMPE}{\mathord{\supset}\textup{E}}
+    \prfMakeInferenceRuleRef{NDIMPIL}{\mathord{\supset}\textup{I}}
   \else
-    \def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\rightarrow}%
-        \textup{I}$}}
-    \def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\rightarrow}%
-        \textup{E}$}}
-    \def\NDIMPIL#1{%
-      \prftree[by]{$\scriptstyle\mathord{\rightarrow}%
-        \textup{I}^{\prfref<#1>}$}}\fi
-  \def\NDNOTI{\prftree[by]{$\scriptstyle\mathord{\neg}%
-      \textup{I}$}}
-  \def\NDNOTIL#1{\prftree[by]{$\scriptstyle{\neg}%
-      \textup{I}^{\prfref<#1>}$}}
-  \def\NDNOTE{\prftree[by]{$\scriptstyle\mathord{\neg}%
-      \textup{E}$}}
-  \def\NDALLI{\prftree[by]{$\scriptstyle\mathord{\forall}%
-      \textup{I}$}}
-  \def\NDALLE{\prftree[by]{$\scriptstyle\mathord{\forall}%
-      \textup{E}$}}
-  \def\NDEXI{\prftree[by]{$\scriptstyle\mathord{\exists}%
-      \textup{I}$}}
-  \def\NDEXE{\prftree[by]{$\scriptstyle\mathord{\exists}%
-      \textup{E}$}}
-  \def\NDEXEL#1{%
-    \prftree[by]{$\scriptstyle\mathord{\exists}%
-      \textup{E}^{\prfref<#1>}$}}
-  \def\NDTI{\prftree[by]{$\scriptstyle\mathord{\top}%
-      \textup{I}$}}
-  \def\NDFE{\prftree[by]{$\scriptstyle\mathord{\bot}%
-      \textup{E}$}}
-  \def\NDLEM{\prftree[by]{$\scriptstyle\textup{lem}$}}
-  \def\NDAX{\prftree[by]{$\scriptstyle\textup{ax}$}}
+    \prfMakeInferenceRule{NDIMPI}{\mathord{\rightarrow}\textup{I}}
+    \prfMakeInferenceRule{NDIMPE}{\mathord{\rightarrow}\textup{E}}
+    \prfMakeInferenceRuleRef{NDIMPIL}{\mathord{\rightarrow}\textup{I}}
+  \fi
+  \prfMakeInferenceRule{NDNOTI}{\mathord{\neg}\textup{I}}
+  \prfMakeInferenceRuleRef{NDNOTIL}{\mathord{\neg}\textup{I}}
+  \prfMakeInferenceRule{NDNOTE}{\mathord{\neg}\textup{E}}
+  \prfMakeInferenceRule{NDALLI}{\mathord{\forall}\textup{I}}
+  \prfMakeInferenceRule{NDALLE}{\mathord{\forall}\textup{E}}
+  \prfMakeInferenceRule{NDEXI}{\mathord{\exists}\textup{I}}
+  \prfMakeInferenceRule{NDEXE}{\mathord{\exists}\textup{E}}
+  \prfMakeInferenceRuleRef{NDEXEL}{\mathord{\exists}\textup{E}}
+  \prfMakeInferenceRule{NDTI}{\mathord{\top}\textup{I}}
+  \prfMakeInferenceRule{NDFE}{\mathord{\bot}\textup{E}}
+  \prfMakeInferenceRule{NDLEM}{\textup{lem}}
+  \prfMakeInferenceRule{NDAX}{\textup{ax}}
 \fi
 
 % -------------------------------------------------------------------
@@ -1064,41 +1073,374 @@
 \ifprf@SEQOption%
   \def\SEQA{\prfassumption}
   \def\SEQD{\prfboundedassumption}
-  \def\SEQP{\prftree}
-  \def\SEQAX{\prftree[by]{$\scriptstyle\textup{Ax}$}}
-  \def\SEQLF{\prftree[by]{$\scriptstyle\textup{L}\bot$}}
-  \def\SEQLW{\prftree[by]{$\scriptstyle\textup{LW}$}}
-  \def\SEQRW{\prftree[by]{$\scriptstyle\textup{RW}$}}
-  \def\SEQLC{\prftree[by]{$\scriptstyle\textup{LC}$}}
-  \def\SEQRC{\prftree[by]{$\scriptstyle\textup{RC}$}}
-  \def\SEQLAND{\prftree[by]{$\scriptstyle\textup{L}%
-      \mathord{\wedge}$}}
-  \def\SEQRAND{\prftree[by]{$\scriptstyle\textup{R}%
-      \mathord{\wedge}$}}
-  \def\SEQLOR{\prftree[by]{$\scriptstyle\textup{L}%
-      \mathord{\vee}$}}
-  \def\SEQROR{\prftree[by]{$\scriptstyle\textup{R}%
-      \mathord{\vee}$}}
+  \def\SEQP{\prftree} 
+  \prfMakeInferenceRule{SEQAX}{\textup{Ax}}
+  \prfMakeInferenceRule{SEQLF}{\textup{L}\mathord{\bot}}
+  \prfMakeInferenceRule{SEQLW}{\textup{LW}}
+  \prfMakeInferenceRule{SEQRW}{\textup{RW}}
+  \prfMakeInferenceRule{SEQLC}{\textup{LC}}
+  \prfMakeInferenceRule{SEQRC}{\textup{RC}}
+  \prfMakeInferenceRule{SEQLAND}{\textup{L}\mathord{\wedge}}
+  \prfMakeInferenceRule{SEQLANDL}{\textup{L}\mathord{\wedge}_1}
+  \prfMakeInferenceRule{SEQLANDR}{\textup{L}\mathord{\wedge}_2}
+  \prfMakeInferenceRule{SEQRAND}{\textup{R}\mathord{\wedge}}
+  \prfMakeInferenceRule{SEQLOR}{\textup{L}\mathord{\vee}}
+  \prfMakeInferenceRule{SEQROR}{\textup{R}\mathord{\vee}}
+  \prfMakeInferenceRule{SEQRORL}{\textup{R}\mathord{\vee}_1}
+  \prfMakeInferenceRule{SEQRORR}{\textup{R}\mathord{\vee}_2}
   \ifprfIMPOption
-    \def\SEQLIMP{\prftree[by]{$\scriptstyle\textup{L}%
-        \mathord{\supset}$}}
-    \def\SEQRIMP{\prftree[by]{$\scriptstyle\textup{R}%
-        \mathord{\supset}$}}
+    \prfMakeInferenceRule{SEQLIMP}{\textup{L}\mathord{\supset}}
+    \prfMakeInferenceRule{SEQRIMP}{\textup{R}\mathord{\supset}}
   \else
-    \def\SEQLIMP{\prftree[by]{$\scriptstyle\textup{L}%
-        \mathord{\rightarrow}$}}
-    \def\SEQRIMP{\prftree[by]{$\scriptstyle\textup{R}%
-        \mathord{\rightarrow}$}}
+    \prfMakeInferenceRule{SEQLIMP}{\textup{L}\mathord{\rightarrow}}
+    \prfMakeInferenceRule{SEQRIMP}{\textup{R}\mathord{\rightarrow}}
   \fi
-  \def\SEQLALL{\prftree[by]{$\scriptstyle\textup{L}%
-      \mathord{\forall}$}} 
-  \def\SEQRALL{\prftree[by]{$\scriptstyle\textup{R}%
-      \mathord{\forall}$}}
-  \def\SEQLEX{\prftree[by]{$\scriptstyle\textup{L}%
-      \mathord{\exists}$}}
-  \def\SEQREX{\prftree[by]{$\scriptstyle\textup{R}%
-      \mathord{\exists}$}}
-  \def\SEQCUT{\prftree[by]{$\scriptstyle\textup{Cut}$}}
+  \prfMakeInferenceRule{SEQLALL}{\textup{L}\mathord{\forall}}
+  \prfMakeInferenceRule{SEQRALL}{\textup{R}\mathord{\forall}}
+  \prfMakeInferenceRule{SEQLEX}{\textup{L}\mathord{\exists}}
+  \prfMakeInferenceRule{SEQREX}{\textup{R}\mathord{\exists}}
+  \prfMakeInferenceRule{SEQCUT}{\textup{Cut}}
 \fi
 
 % -------------------------------------------------------------------
+% Equality rules
+%
+% Package option [EQ]
+% -------------------------------------------------------------------
+
+\ifprf@EQOption%
+  \prfMakeInferenceRule{EQREFL}{\textup{refl}}
+  \prfMakeInferenceRule{EQSYM}{\textup{sym}}
+  \prfMakeInferenceRule{EQTRANS}{\textup{trans}}
+  \prfMakeInferenceRule{EQSUBST}{\textup{subst}}
+\fi
+
+% -------------------------------------------------------------------
+% Martin-Lof and Homotopy Type Theory
+%
+% Package option [ML]
+% -------------------------------------------------------------------
+
+\ifprf@MLOption
+  \ifprf@MLnodefOption\relax\else
+    \def\type{\mathbin{:}}
+    \def\universe{\mathcal{U}}
+    \def\context{\mathsf{ctx}}
+    \def\judgementaldef{\mathbin{:\equiv}}
+    \def\propositionaldef{\mathbin{:=}}
+    \def\identitytype{\mathsf{Id}}
+    \def\refl{\mathsf{refl}}
+    \def\emptytype{\mathbf{0}}
+    \def\unittype{\mathbf{1}}
+    \def\booleantype{\mathbf{2}}
+    \def\axiomofchoice{\mathsf{AC}}
+    \def\accessibility{\mathsf{acc}}
+    \def\ap{\mathsf{ap}}
+    \def\apd{\mathsf{apd}}
+    \def\basepoint{\mathsf{base}}
+    \def\biinv{\mathsf{biinv}}
+    \def\cardtype{\mathsf{Card}}
+    \def\cocone{\mathsf{cocone}}
+    \def\cons{\mathsf{cons}}
+    \def\contr{\mathsf{contr}}
+    \def\equivtype{\mathsf{Equiv}}
+    \def\ext{\mathsf{ext}}
+    \def\fiber{\mathsf{fib}}
+    \def\funext{\mathsf{funext}}
+    \def\glue{\mathsf{glue}}
+    \def\happly{\mathsf{happly}}
+    \def\hom{\mathsf{hom}}
+    \def\id{\mathsf{id}}
+    \def\idtoeqv{\mathsf{idtoeqv}}
+    \def\idtoiso{\mathsf{idtoiso}}
+    \def\im{\mathsf{im}}
+    \def\ind{\mathsf{ind}}
+    \def\inj{\mathsf{inj}}
+    \def\inl{\mathsf{inl}}
+    \def\inr{\mathsf{inr}}
+    \def\iscontr{\mathsf{isContr}}
+    \def\isequiv{\mathsf{isequiv}}
+    \def\ishae{\mathsf{ishae}}
+    \def\isotoid{\mathsf{istoid}}
+    \def\isntype#1{\mathsf{is-}{#1}\mathsf{-type}}
+    \def\isprop{\mathsf{isProp}}
+    \def\isset{\mathsf{isSet}}
+    \def\ker{\mathsf{ker}}
+    \def\LEM{\mathsf{LEM}}
+    \def\linv{\mathsf{linv}}
+    \def\listtype{\mathsf{List}}
+    \def\loopcons{\mathsf{loop}}
+    \def\Map{\mathsf{Map}}
+    \def\merid{\mathsf{merid}}
+    \def\nil{\mathsf{nil}}
+    \def\ordtype{\mathsf{Ord}}
+    \def\pair{\mathsf{pair}}
+    \def\pred{\mathsf{pred}}
+    \def\pr{\mathsf{pr}}
+    \def\Prop{\mathsf{Prop}}
+    \def\qinv{\mathsf{qinv}}
+    \def\rec{\mathsf{rec}}
+    \def\rinv{\mathsf{rinv}}
+    \def\seg{\mathsf{seg}}
+    \def\Set{\mathsf{Set}}
+    \def\Succ{\mathsf{succ}}
+    \def\sup{\mathsf{sup}}
+    \def\total{\mathsf{total}}
+    \def\transport{\mathsf{transport}}
+    \def\transportconst{\mathsf{transportconst}}
+    \def\ua{\mathsf{ua}}
+    \def\Wtype{\mathsf{W}}
+  \fi
+  
+  \def\MLctxEMPrule{\ensuremath{\mathsf{ctx}\mathsf{-EMP}}}
+  \def\MLctxEXTrule{\ensuremath{\mathsf{ctx}\mathsf{-EXT}}}
+  \def\MLVblerule{\ensuremath{\mathsf{Vble}}}
+  \def\MLSubstrule{\ensuremath{\mathsf{Subst}}}
+  \def\MLWkgrule{\ensuremath{\mathsf{Wkg}}}
+  \def\MLEQreflrule{\ensuremath{\mathord{\equiv}\mathsf{-refl}}}
+  \def\MLEQsymrule{\ensuremath{\mathord{\equiv}\mathsf{-sym}}}
+  \def\MLEQtransrule{\ensuremath{\mathord{\equiv}\mathsf{-trans}}}
+  \def\MLEQsubstrule{\ensuremath{\mathord{\equiv}\mathsf{-subst}}}
+  \def\MLEQsubsteqrule{\ensuremath{\mathord{\equiv}%
+      \mathsf{-subst}\mathsf{-eq}}}
+  \def\MLUintrorule{\ensuremath{\universe\mathsf{-intro}}}
+  \def\MLUcumulrule{\ensuremath{\universe\mathsf{-cumul}}}
+  \def\MLUcumuleqrule{\ensuremath{\universe%
+      \mathsf{-cumul}\mathsf{-eq}}}
+  \def\MLpiformrule{\ensuremath{\Pi\mathsf{-form}}}
+  \def\MLpiformeqrule{\ensuremath{\Pi\mathsf{-form}\mathsf{-eq}}}
+  \def\MLpiintrorule{\ensuremath{\Pi\mathsf{-intro}}}
+  \def\MLpiintroeqrule{\ensuremath{\Pi\mathsf{-intro}\mathsf{-eq}}}
+  \def\MLpielimrule{\ensuremath{\Pi\mathsf{-elim}}}
+  \def\MLpielimeqrule{\ensuremath{\Pi\mathsf{-elim}\mathsf{-eq}}}
+  \def\MLpicomprule{\ensuremath{\Pi\mathsf{-comp}}}
+  \def\MLpiuniqrule{\ensuremath{\Pi\mathsf{-uniq}}}
+  \def\MLKintrorule{\ensuremath{k\mathsf{-intro}}}
+  \def\MLsigmaformrule{\ensuremath{\Sigma\mathsf{-form}}}
+  \def\MLsigmaintrorule{\ensuremath{\Sigma\mathsf{-intro}}}
+  \def\MLsigmaelimrule{\ensuremath{\Sigma\mathsf{-elim}}}
+  \def\MLsigmacomprule{\ensuremath{\Sigma\mathsf{-comp}}}
+  \def\MLsigmauniqrule{\ensuremath{\Sigma\mathsf{-uniq}}}
+  \def\MLplusformrule{\ensuremath{\mathord{+}\mathsf{-form}}}
+  \def\MLplusintrolrule{\ensuremath{\mathord{+}\mathsf{-intro}_1}}
+  \def\MLplusintrorrule{\ensuremath{\mathord{+}\mathsf{-intro}_2}}
+  \def\MLpluselimrule{\ensuremath{\mathord{+}\mathsf{-elim}}}
+  \def\MLpluscomplrule{\ensuremath{\mathord{+}\mathsf{-comp}_1}}
+  \def\MLpluscomprrule{\ensuremath{\mathord{+}\mathsf{-comp}_2}}
+  \def\MLplusuniqrule{\ensuremath{\mathord{+}\mathsf{-uniq}}}
+  \def\MLzeroformrule{\ensuremath{\mathbf{0}\mathsf{-form}}}
+  \def\MLzeroelimrule{\ensuremath{\mathbf{0}\mathsf{-elim}}}
+  \def\MLzerouniqrule{\ensuremath{\mathbf{0}\mathsf{-uniq}}}
+  \def\MLunitformrule{\ensuremath{\mathbf{1}\mathsf{-form}}}
+  \def\MLunitintrorule{\ensuremath{\mathbf{1}\mathsf{-intro}}}
+  \def\MLunitelimrule{\ensuremath{\mathbf{1}\mathsf{-elim}}}
+  \def\MLunitcomprule{\ensuremath{\mathbf{1}\mathsf{-comp}}}
+  \def\MLunituniqrule{\ensuremath{\mathbf{1}\mathsf{-uniq}}}
+  \def\MLnatformrule{\ensuremath{\mathbb{N}\mathsf{-form}}}
+  \def\MLnatintrozerorule{\ensuremath{\mathbb{N}\mathsf{-intro}_1}}
+  \def\MLnatintrosuccrule{\ensuremath{\mathbb{N}\mathsf{-intro}_2}}
+  \def\MLnatelimrule{\ensuremath{\mathbb{N}\mathsf{-elim}}}
+  \def\MLnatcompzerorule{\ensuremath{\mathbb{N}\mathsf{-comp}_1}}
+  \def\MLnatcompsuccrule{\ensuremath{\mathbb{N}\mathsf{-comp}_2}}
+  \def\MLnatuniqrule{\ensuremath{\mathbb{N}\mathsf{-uniq}}}
+  \def\MLidformrule{\ensuremath{\mathord{=}\mathsf{-form}}}
+  \def\MLidintrorule{\ensuremath{\mathord{=}\mathsf{-intro}}}
+  \def\MLidelimrule{\ensuremath{\mathord{=}\mathsf{-elim}}}
+  \def\MLidcomprule{\ensuremath{\mathord{=}\mathsf{-comp}}}
+  \def\MLiduniqrule{\ensuremath{\mathord{=}\mathsf{-uniq}}}
+  \def\MLwformrule{\ensuremath{\mathsf{W}\mathsf{-form}}}
+  \def\MLwintrorule{\ensuremath{\mathsf{W}\mathsf{-intro}}}
+  \def\MLwelimrule{\ensuremath{\mathsf{W}\mathsf{-elim}}}
+  \def\MLwcomprule{\ensuremath{\mathsf{W}\mathsf{-comp}}}
+  \def\MLwuniqrule{\ensuremath{\mathsf{W}\mathsf{-uniq}}}
+  \def\MLListformrule{\ensuremath{\mathsf{List}\mathsf{-form}}}
+  \def\MLListintronrule{\ensuremath{\mathsf{List}\mathsf{-intro_1}}}
+  \def\MLListintrocrule{\ensuremath{\mathsf{List}\mathsf{-intro_2}}}
+  \def\MLListelimrule{\ensuremath{\mathsf{List}\mathsf{-elim}}}
+  \def\MLListcompnrule{\ensuremath{\mathsf{List}\mathsf{-comp_1}}}
+  \def\MLListcompcrule{\ensuremath{\mathsf{List}\mathsf{-comp_2}}}
+  \def\MLListuniqrule{\ensuremath{\mathsf{List}\mathsf{-uniq}}}
+  \def\MLfunextrule{\ensuremath{\Pi\mathsf{-ext}}}
+  \def\MLunivrule{\ensuremath{\universe_i\mathsf{-univ}}}
+  \def\MLSformrule{\ensuremath{\mathbb{S}^1\mathsf{-form}}}
+  \def\MLSintrorule{\ensuremath{\mathbb{S}^1\mathsf{-intro}}}
+  \def\MLSelimrule{\ensuremath{\mathbb{S}^1\mathsf{-elim}}}
+  \def\MLScomprule{\ensuremath{\mathbb{S}^1\mathsf{-comp}}}
+  \def\MLSuniqrule{\ensuremath{\mathbb{S}^1\mathsf{-uniq}}}
+  \def\MLSpeqintrorule{\ensuremath{\mathbb{S}^1\mathsf{-intro}%
+      \mathsf{-}\mathsf{=}}}
+  \def\MLSpeqcomprule{\ensuremath{\mathbb{S}^1\mathsf{-comp}%
+      \mathsf{-}\mathsf{=}}}
+  \def\MLIformrule{\ensuremath{I\mathsf{-form}}}
+  \def\MLIintroarule{\ensuremath{I\mathsf{-intro}_1}}
+  \def\MLIintrobrule{\ensuremath{I\mathsf{-intro}_2}}
+  \def\MLIelimrule{\ensuremath{I\mathsf{-elim}}}
+  \def\MLIcomparule{\ensuremath{I\mathsf{-comp}_1}}
+  \def\MLIcompbrule{\ensuremath{I\mathsf{-comp}_2}}
+  \def\MLIuniqrule{\ensuremath{I\mathsf{-uniq}}}
+  \def\MLIpeqintrorule{\ensuremath{I\mathsf{-intro}%
+      \mathsf{-}\mathsf{=}}}
+  \def\MLIpeqcomprule{\ensuremath{I\mathsf{-comp}{-}\mathsf{=}}}
+  \def\MLsigmaintroarule{\ensuremath{\Sigma\mathsf{-intro}_1}}
+  \def\MLsigmaintrobrule{\ensuremath{\Sigma\mathsf{-intro}_2}}
+  \def\MLsigmacomparule{\ensuremath{\Sigma\mathsf{-comp}_1}}
+  \def\MLsigmacompbrule{\ensuremath{\Sigma\mathsf{-comp}_2}}
+  \def\MLsigmapeqintrorule{\ensuremath{\Sigma\mathsf{-intro}%
+      \mathsf{-}\mathsf{=}}}
+  \def\MLsigmapeqcomprule{\ensuremath{\Sigma\mathsf{-comp}%
+      \mathsf{-}\mathsf{=}}}
+  \def\MLPOformrule{\ensuremath{\sqcup\mathsf{-form}}}
+  \def\MLPOintroarule{\ensuremath{\sqcup\mathsf{-intro}_1}}
+  \def\MLPOintrobrule{\ensuremath{\sqcup\mathsf{-intro}_2}}
+  \def\MLPOelimrule{\ensuremath{\sqcup\mathsf{-elim}}}
+  \def\MLPOcomparule{\ensuremath{\sqcup\mathsf{-comp}_1}}
+  \def\MLPOcompbrule{\ensuremath{\sqcup\mathsf{-comp}_2}}
+  \def\MLPOuniqrule{\ensuremath{\sqcup\mathsf{-uniq}}}
+  \def\MLPOpeqintrorule{\ensuremath{\sqcup\mathsf{-intro}%
+      \mathsf{-}\mathsf{=}}}
+  \def\MLPOpeqcomprule{\ensuremath{\sqcup%
+      \mathsf{-comp}\mathsf{-}\mathsf{=}}}
+  \def\MLTformrule{\ensuremath{||\cdot||\mathsf{-form}}}
+  \def\MLTintrorule{\ensuremath{||\cdot||\mathsf{-intro}}}
+  \def\MLTelimrule{\ensuremath{||\cdot||\mathsf{-elim}}}
+  \def\MLTcomprule{\ensuremath{||\cdot||\mathsf{-comp}}}
+  \def\MLTuniqrule{\ensuremath{||\cdot||\mathsf{-uniq}}}
+  \def\MLTpeqintrorule{\ensuremath{||\cdot||\mathsf{-intro}%
+      \mathsf{-}\mathsf{=}}}
+  \def\MLTpeqcomprule{\ensuremath{||\cdot||\mathsf{-comp}%
+      \mathsf{-}\mathsf{=}}}
+  \def\MLtorusformrule{\ensuremath{T^2\mathsf{-form}}}
+  \def\MLtorusintrorule{\ensuremath{T^2\mathsf{-intro}}}
+  \def\MLtoruselimrule{\ensuremath{T^2\mathsf{-elim}}}
+  \def\MLtoruscomprule{\ensuremath{T^2\mathsf{-comp}}}
+  \def\MLtoruspeqintroarule{\ensuremath{T^2\mathsf{-intro}%
+      \mathsf{-}\mathsf{=_p}}}
+  \def\MLtoruspeqintrobrule{\ensuremath{T^2\mathsf{-intro}%
+      \mathsf{-}\mathsf{=_q}}}
+  \def\MLtoruspeqintrocrule{\ensuremath{T^2\mathsf{-intro}%
+      \mathsf{-}\mathsf{=_t}}}
+  \def\MLtoruspeqcomparule{\ensuremath{T^2\mathsf{-comp}%
+      \mathsf{-}\mathsf{=_p}}}
+  \def\MLtoruspeqcompbrule{\ensuremath{T^2\mathsf{-comp}%
+      \mathsf{-}\mathsf{=_q}}}
+  \def\MLtoruspeqcompcrule{\ensuremath{T^2\mathsf{-comp}%
+      \mathsf{-}\mathsf{=_t}}}
+  
+  \prfMakeInferenceRule{MLctxEMP}{\MLctxEMPrule}
+  \prfMakeInferenceRule{MLctxEXT}{\MLctxEXTrule}
+  \prfMakeInferenceRule{MLSubst}{\MLSubstrule}
+  \prfMakeInferenceRule{MLWkg}{\MLWkgrule}
+  \prfMakeInferenceRule{MLVble}{\MLVblerule}
+  \prfMakeInferenceRule{MLEQrefl}{\MLEQreflrule}
+  \prfMakeInferenceRule{MLEQsym}{\MLEQsymrule} 
+  \prfMakeInferenceRule{MLEQtrans}{\MLEQtransrule}
+  \prfMakeInferenceRule{MLEQsubst}{\MLEQsubstrule}
+  \prfMakeInferenceRule{MLEQsubsteq}{\MLEQsubsteqrule}
+  \prfMakeInferenceRule{MLUintro}{\MLUintrorule}
+  \prfMakeInferenceRule{MLUcumul}{\MLUcumulrule}
+  \prfMakeInferenceRule{MLUcumuleq}{\MLUcumuleqrule}
+  \prfMakeInferenceRule{MLpiform}{\MLpiformrule}
+  \prfMakeInferenceRule{MLpiformeq}{\MLpiformeqrule}
+  \prfMakeInferenceRule{MLpiintro}{\MLpiintrorule}
+  \prfMakeInferenceRule{MLpiintroeq}{\MLpiintroeqrule}
+  \prfMakeInferenceRule{MLpielim}{\MLpielimrule}
+  \prfMakeInferenceRule{MLpielimeq}{\MLpielimeqrule}
+  \prfMakeInferenceRule{MLpicomp}{\MLpicomprule}
+  \prfMakeInferenceRule{MLpiuniq}{\MLpiuniqrule}
+  \prfMakeInferenceRule{MLKintro}{\MLKintrorule}
+  \prfMakeInferenceRule{MLsigmaform}{\MLsigmaformrule}
+  \prfMakeInferenceRule{MLsigmaintro}{\MLsigmaintrorule}
+  \prfMakeInferenceRule{MLsigmaelim}{\MLsigmaelimrule}
+  \prfMakeInferenceRule{MLsigmacomp}{\MLsigmacomprule}
+  \prfMakeInferenceRule{MLsigmauniq}{\MLsigmauniqrule}
+  \prfMakeInferenceRule{MLplusform}{\MLplusformrule}
+  \prfMakeInferenceRule{MLplusintrol}{\MLplusintrolrule}
+  \prfMakeInferenceRule{MLplusintror}{\MLplusintrorrule}
+  \prfMakeInferenceRule{MLpluselim}{\MLpluselimrule}
+  \prfMakeInferenceRule{MLpluscompl}{\MLpluscomplrule}
+  \prfMakeInferenceRule{MLpluscompr}{\MLpluscomprrule}
+  \prfMakeInferenceRule{MLplusuniq}{\MLplusuniqrule}
+  \prfMakeInferenceRule{MLzeroform}{\MLzeroformrule}
+  \prfMakeInferenceRule{MLzeroelim}{\MLzeroelimrule}
+  \prfMakeInferenceRule{MLzerouniq}{\MLzerouniqrule}
+  \prfMakeInferenceRule{MLunitform}{\MLunitformrule}
+  \prfMakeInferenceRule{MLunitintro}{\MLunitintrorule}
+  \prfMakeInferenceRule{MLunitelim}{\MLunitelimrule}
+  \prfMakeInferenceRule{MLunitcomp}{\MLunitcomprule}
+  \prfMakeInferenceRule{MLunituniq}{\MLunituniqrule}
+  \prfMakeInferenceRule{MLnatform}{\MLnatformrule}
+  \prfMakeInferenceRule{MLnatintrozero}{\MLnatintrozerorule}
+  \prfMakeInferenceRule{MLnatintrosucc}{\MLnatintrosuccrule}
+  \prfMakeInferenceRule{MLnatelim}{\MLnatelimrule}
+  \prfMakeInferenceRule{MLnatcompzero}{\MLnatcompzerorule}
+  \prfMakeInferenceRule{MLnatcompsucc}{\MLnatcompsuccrule}
+  \prfMakeInferenceRule{MLnatuniq}{\MLnatuniqrule}
+  \prfMakeInferenceRule{MLidform}{\MLidformrule}
+  \prfMakeInferenceRule{MLidintro}{\MLidintrorule}
+  \prfMakeInferenceRule{MLidelim}{\MLidelimrule}
+  \prfMakeInferenceRule{MLidcomp}{\MLidcomprule}
+  \prfMakeInferenceRule{MLiduniq}{\MLiduniqrule}
+  \prfMakeInferenceRule{MLwform}{\MLwformrule}
+  \prfMakeInferenceRule{MLwintro}{\MLwintrorule}
+  \prfMakeInferenceRule{MLwelim}{\MLwelimrule}
+  \prfMakeInferenceRule{MLwcomp}{\MLwcomprule}
+  \prfMakeInferenceRule{MLwuniq}{\MLwuniqrule}
+  \prfMakeInferenceRule{MLListform}{\MLListformrule}
+  \prfMakeInferenceRule{MLListintron}{\MLListintronrule}
+  \prfMakeInferenceRule{MLListintroc}{\MLListintrocrule}
+  \prfMakeInferenceRule{MLListelim}{\MLListelimrule}
+  \prfMakeInferenceRule{MLListcompn}{\MLListcompnrule}
+  \prfMakeInferenceRule{MLListcompc}{\MLListcompcrule}
+  \prfMakeInferenceRule{MLListuniq}{\MLListuniqrule}
+  \prfMakeInferenceRule{MLfunext}{\MLfunextrule}
+  \prfMakeInferenceRule{MLuniv}{\MLunivrule}
+  \prfMakeInferenceRule{MLSform}{\MLSformrule}
+  \prfMakeInferenceRule{MLSintro}{\MLSintrorule}
+  \prfMakeInferenceRule{MLSelim}{\MLSelimrule}
+  \prfMakeInferenceRule{MLScomp}{\MLScomprule}
+  \prfMakeInferenceRule{MLSuniq}{\MLSuniqrule}
+  \prfMakeInferenceRule{MLSpeqintro}{\MLSpeqintrorule}
+  \prfMakeInferenceRule{MLSpeqcomp}{\MLSpeqcomprule}
+  \prfMakeInferenceRule{MLIform}{\MLIformrule}
+  \prfMakeInferenceRule{MLIintroa}{\MLIintroarule}
+  \prfMakeInferenceRule{MLIintrob}{\MLIintrobrule}
+  \prfMakeInferenceRule{MLIelim}{\MLIelimrule}
+  \prfMakeInferenceRule{MLIcompa}{\MLIcomparule}
+  \prfMakeInferenceRule{MLIcompb}{\MLIcompbrule}
+  \prfMakeInferenceRule{MLIuniq}{\MLIuniqrule}
+  \prfMakeInferenceRule{MLIpeqintro}{\MLIpeqintrorule}
+  \prfMakeInferenceRule{MLIpeqcomp}{\MLIpeqcomprule}
+  \prfMakeInferenceRule{MLsigmaintroa}{\MLsigmaintroarule}
+  \prfMakeInferenceRule{MLsigmaintrob}{\MLsigmaintrobrule}
+  \prfMakeInferenceRule{MLsigmacompa}{\MLsigmacomparule}
+  \prfMakeInferenceRule{MLsigmacompb}{\MLsigmacompbrule}
+  \prfMakeInferenceRule{MLsigmapeqintro}{\MLsigmapeqintrorule}
+  \prfMakeInferenceRule{MLsigmapeqcomp}{\MLsigmapeqcomprule}
+  \prfMakeInferenceRule{MLPOform}{\MLPOformrule}
+  \prfMakeInferenceRule{MLPOintroa}{\MLPOintroarule}
+  \prfMakeInferenceRule{MLPOintrob}{\MLPOintrobrule}
+  \prfMakeInferenceRule{MLPOelim}{\MLPOelimrule}
+  \prfMakeInferenceRule{MLPOcompa}{\MLPOcomparule}
+  \prfMakeInferenceRule{MLPOcompb}{\MLPOcompbrule}
+  \prfMakeInferenceRule{MLPOuniq}{\MLPOuniqrule}
+  \prfMakeInferenceRule{MLPOpeqintro}{\MLPOpeqintrorule}
+  \prfMakeInferenceRule{MLPOpeqcomp}{\MLPOpeqcomprule}
+  \prfMakeInferenceRule{MLTform}{\MLTformrule}
+  \prfMakeInferenceRule{MLTintro}{\MLTintrorule}
+  \prfMakeInferenceRule{MLTelim}{\MLTelimrule}
+  \prfMakeInferenceRule{MLTcomp}{\MLTcomprule}
+  \prfMakeInferenceRule{MLTuniq}{\MLTuniqrule}
+  \prfMakeInferenceRule{MLTpeqintro}{\MLTpeqintrorule}
+  \prfMakeInferenceRule{MLTpeqcomp}{\MLTpeqcomprule}
+  \prfMakeInferenceRule{MLtorusform}{\MLtorusformrule}
+  \prfMakeInferenceRule{MLtorusintro}{\MLtorusintrorule}
+  \prfMakeInferenceRule{MLtoruselim}{\MLtoruselimrule}
+  \prfMakeInferenceRule{MLtoruscomp}{\MLtoruscomprule}
+  \prfMakeInferenceRule{MLtoruspeqintroa}{\MLtoruspeqintroarule}
+  \prfMakeInferenceRule{MLtoruspeqintrob}{\MLtoruspeqintrobrule}
+  \prfMakeInferenceRule{MLtoruspeqintroc}{\MLtoruspeqintrocrule}
+  \prfMakeInferenceRule{MLtoruspeqcompa}{\MLtoruspeqcomparule}
+  \prfMakeInferenceRule{MLtoruspeqcompb}{\MLtoruspeqcompbrule}
+  \prfMakeInferenceRule{MLtoruspeqcompc}{\MLtoruspeqcompcrule}
+\fi
+% -------------------------------------------------------------------