\newcommand{\id}{(id)}
\newcommand{\idrule}{
 \AxiomC{}
 \LeftLabel{\id}
 \UnaryInfC{$A \vdash A$}
 \DisplayProof
}

\newcommand{\tright}{(\ensuremath{\seq\verum})}
\newcommand{\trightrule}{
 \AxiomC{}
 \LeftLabel{\tright}
 \UnaryInfC{$\seq \verum$}
 \DisplayProof
}

\newcommand{\tleft}{(\ensuremath{\verum\seq})}
\newcommand{\tleftrule}{
 \AxiomC{$\Gamma \seq C$}
 \LeftLabel{\tleft}
 \UnaryInfC{$ \verum , \Gamma \seq C$}
 \DisplayProof
}

\newcommand{\impright}{(\ensuremath{\seq\limp})}
\newcommand{\imprightrule}{
 \AxiomC{$\Gamma, A \vdash B$}
 \LeftLabel{\impright}
 \UnaryInfC{$\Gamma \vdash A \to B$}
 \DisplayProof
}

\newcommand{\impleft}{(\ensuremath{\limp\seq})}
\newcommand{\impleftrule}{
 \AxiomC{$\Gamma_1 \vdash A$}
 \AxiomC{$B, \Gamma_2 \vdash C$}
 \LeftLabel{\impleft}
 \BinaryInfC{$\Gamma_1, A \limp B, \Gamma_2 \vdash C$}
 \DisplayProof
}

\newcommand{\impcleft}{\myb{\limp\seq}}
\newcommand{\impcleftrule}{
 \AxiomC{$\Gamma_1 \seq A$}
 \AxiomC{$B, \Gamma_2 \seq C$}
 \LeftLabel{\impcleft}
 \RightLabel{$\dagger$}
 \BinaryInfC{$\myb{\Gamma_1, A \limp B, \Gamma_2} \seq C$}
 \DisplayProof
}

\newcommand{\strid}{(id\ensuremath{\smsc})}
\newcommand{\stridrule}{
 \AxiomC{}
 \LeftLabel{\strid}
 \UnaryInfC{$A \vdash A$}
 \DisplayProof
}

\newcommand{\strtright}{(\ensuremath{\seq\verum\smsc})}
\newcommand{\strtrightrule}{
 \AxiomC{}
 \LeftLabel{\tright}
 \UnaryInfC{$\seq \verum$}
 \DisplayProof
}

\newcommand{\strmtleft}{(M\ensuremath{_{\verum}\seq\smsc})}
\newcommand{\strmtleftrule}{
 \AxiomC{$\astr{U}{\verum\semic\verum} \seq C$}
 \LeftLabel{\strmtleft}
 \UnaryInfC{$ \astr{U}{\verum} \seq C$}
 \DisplayProof
}

\newcommand{\strkitleft}{(KI\ensuremath{_{\verum}\seq\smsc})}
\newcommand{\strkitleftrule}{
 \AxiomC{$\astr{U}{Y} \seq C$}
 \LeftLabel{\strkitleft}
 \UnaryInfC{$ \astr{U}{\verum \semic Y} \seq C$}
 \DisplayProof
}

%\newcommand{\strktleft}{(K\ensuremath{_{\verum}\seq\smsc})}
\newcommand{\strktleftrule}{
 \AxiomC{$\astr{U}{Y} \seq C$}
 \LeftLabel{\strktleft}
 \UnaryInfC{$ \astr{U}{Y \semic \verum} \seq C$}
 \DisplayProof
}

%\newcommand{\strttleft}{(T\ensuremath{_{\verum}\seq\smsc})}
\newcommand{\strttrightrule}{
 \AxiomC{$\astr{U}{Y \semic\verum} \seq C$}
 \LeftLabel{\strttleft}
 \UnaryInfC{$ \astr{U}{\verum\semic Y} \seq C$}
 \DisplayProof
}


\newcommand{\strimpright}{(\ensuremath{\seq\limp\smsc})}
\newcommand{\strimprightrule}{
 \AxiomC{$U \semic A \vdash B$}
 \LeftLabel{\strimpright}
 \UnaryInfC{$U \vdash A \limp B$}
 \DisplayProof
}

\newcommand{\strimpleft}{(\ensuremath{\limp\seq\smsc})}
\newcommand{\strimpleftrule}{
 \AxiomC{$V \vdash A$}
 \AxiomC{$\astr{U}{B} \vdash C$}
 \LeftLabel{\strimpleft}
 \BinaryInfC{$\astr{U}{A \limp B \semic V} \vdash C$}
 \DisplayProof
}

\newcommand{\strimpcleft}{\myb{\limp\seq\smsc}}
\newcommand{\strimpcleftrule}{
 \AxiomC{$\Gamma_1 \seq A$}
 \AxiomC{$B, \Gamma_2 \seq C$}
 \LeftLabel{\strimpcleft}
 \BinaryInfC{$\myb{\Gamma_1, A \limp B, \Gamma_2} \seq C$}
 \DisplayProof
}

\newcommand{\strcut}{(cut\smsc)}
\newcommand{\strcutrule}{
 \AxiomC{$V \vdash A$}
 \AxiomC{$\astr{U}{A} \vdash C$}
 \LeftLabel{\strcut}
 \BinaryInfC{$\astr{U}{V} \vdash C$}
 \DisplayProof
}

%\newcommand{\strwleft}{(W\ensuremath{\seq\smsc})}
\newcommand{\strwleftrule}{
 \AxiomC{$\astr{U}{X \semic Y \semic Y} \vdash C$}
 \LeftLabel{\strwleft}
 \UnaryInfC{$\astr{U}{X \semic Y} \vdash C$}
 \DisplayProof
}

%\newcommand{\strbleft}{(B\ensuremath{\seq\smsc})}
\newcommand{\strbleftrule}{
 \AxiomC{$\astr{U}{X \semic (Y \semic Z)} \vdash C$}
 \LeftLabel{\strbleft}
 \UnaryInfC{$\astr{U}{X \semic Y \semic Z} \vdash C$}
 \DisplayProof
}

%\newcommand{\strbpleft}{(B\ensuremath{'\seq\smsc})}
\newcommand{\strbpleftrule}{
 \AxiomC{$\astr{U}{X \semic (Z \semic Y)} \vdash C$}
 \LeftLabel{\strbpleft}
 \UnaryInfC{$\astr{U}{Z \semic X \semic Y} \vdash C$}
 \DisplayProof
}

\newcommand{\strcleft}{(C\ensuremath{\seq\smsc})}
\newcommand{\strcleftrule}{
 \AxiomC{$\astr{U}{X \semic Z \semic Y} \vdash C$}
 \LeftLabel{\strcleft}
 \UnaryInfC{$\astr{U}{X \semic Y \semic Z} \vdash C$}
 \DisplayProof
}

\newcommand{\strcileft}{(CI\ensuremath{\seq\smsc})}
\newcommand{\strcileftrule}{
 \AxiomC{$\astr{U}{Y \semic X} \vdash C$}
 \LeftLabel{\strcileft}
 \UnaryInfC{$\astr{U}{X \semic Y} \vdash C$}
 \DisplayProof
}

\newcommand{\cut}{(cut)}
\newcommand{\cutrule}{
 \AxiomC{$\Gamma_1 \vdash A$}
 \AxiomC{$A, \Gamma_2 \vdash C$}
 \LeftLabel{\cut}
 \BinaryInfC{$\Gamma_1, \Gamma_2 \vdash C$}
 \DisplayProof
}

\newcommand{\wleft}{(W\ensuremath{\seq})}
\newcommand{\wleftrule}{
 \AxiomC{$\Gamma, A, A\vdash C$}
 \LeftLabel{\wleft}
 \UnaryInfC{$\Gamma, A \vdash C$}
 \DisplayProof
}

