To define the sums (disjoint union) of two predicates, we extend
the language with two unary function symbols inl x and inr x . ![\begin{sort}[]~
\begin{center}sum['a,'b]
\end{center}\end{sort}](img120.png)
![\begin{constant}[]~
\begin{center}%
\afdmath{}\text{\rm inl}\endafdmath{} : 'a $...
...'a, 'b]
\SaveVerb{Verb}inl\marginpar{\UseVerb{Verb}}\end{center}\end{constant}](img121.png)
![\begin{constant}[]~
\begin{center}%
\afdmath{}\text{\rm inr}\endafdmath{} : 'b $...
...'a, 'b]
\SaveVerb{Verb}inr\marginpar{\UseVerb{Verb}}\end{center}\end{constant}](img122.png)
![\begin{definition}[ Sum of predicates ]~
\begin{center}%
\afdmath{}(\text{\it A}...
...\SaveVerb{Verb}Sum A B z\marginpar{\UseVerb{Verb}}\end{center}\end{definition}](img123.png)
![\begin{axiom}[ ]\hspace{1cm}
\begin{itemize}
\item %
\afdmath{}\text{\rm inl}.\t...
...box{}\endprettybox{}\endprettybox{}\endafdmmath{}}
\par
\end{itemize}\end{axiom}](img124.png)
inl_not_inr.Sum added as elimination rule (abbrev: inl_not_inr , options: -i -n )
The last claim is added as invertible elimination rule.
![\begin{fact}[ Introduction rules for sums ]\hspace{1cm}
\begin{itemize}
\item %
...
...tion rule (abbrev: \verb ...](img125.png)
![\begin{fact}[ elimination rules for sums ]\hspace{1cm}
\begin{itemize}
\item %
\...
...ev: \verb ...](img126.png)
These four rules and are added as invertible elimination rules.