# Theory SingleSuccedent

section "Single Succedent"
theory SingleSuccedent
imports "HOL-Library.Multiset"
begin
text‹
\section{Single Succedent Calculi \label{isasingle}}
We must be careful when restricting sequents to single succedents. If we have sequents as a pair of multisets, where the second is restricted to having size at most 1, then how does one extend the active part of $\implies{L}{}$ from \textbf{G3ip}? The left premiss will be $\implies{A}{B} \Rightarrow A$, and the extension will be $\Gamma \Rightarrow C$. The \texttt{extend} function must be able to correctly choose to discard the $C$.
Rather than taking this route, we instead restrict to single formulae in the succedents of sequents. This raises its own problems, since now how does one represent the empty succedent? We introduce a dummy formula \texttt{Em}, which will stand for the empty formula:
›