+\newcommand*\ConvertS[3]{#2\ld@converts{#1}#3}
+\newcommand*\ConvertSA[4]{#2\ld@env{#1}#3\ld@converts{#1}#4}
+\newcommand*\CoPremise[4]{\ld@copremise{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
+\newcommand*\CoWeightA[2]{\ld@coweight{#1}\ld@tuple@a{#1}{#2}}
+\newcommand*\CoWeightB[3]{\ld@coweight{#1}\ld@tuple@b{#1}{#2}{#3}}
+\newcommand*\Drop[3]{\ld@drop{#1}{}#2\ld@eq{#1}#3}
+\newcommand*\DropA[4]{\ld@drop{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
+\newcommand*\DropB[5]{\ld@drop{#1}{\ld@tuple@b{#1}{#2}{#3}}#4\ld@eq{#1}#5}
+\newcommand*\DropS[4]{\ld@drops{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
+\renewcommand*\Equiv[3]{#2\ld@equiv{#1}{}#3}
+\newcommand*\EquivA[4]{#3\ld@equiv{#1}{\ld@tuple@a{#1}{#2}}#4}
+\newcommand*\Flat[2]{\ld@flat{#1}\ld@tuple@a{#1}{#2}}
+\newcommand*\FunLift[4]{\ld@funlift{#1}{\ld@tuple@b{#1}{#2}{#3}}#4}
+\newcommand*\FunLiftS[3]{\ld@funlifts{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\FunSubstS[4]{\mathop{\ld@ob{#1}#3\ld@substs{#1}#2\ld@cb{#1}}#4}
+\newcommand*\FunV[3]{\ld@funv{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\FunW[3]{\ld@funw{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\LEnv[2]{\ld@lenv{#1}#2}
+\newcommand*\Length[2]{\ld@length@open{#1}#2\ld@length@close{#1}}
+\newcommand*\Level[2]{\ld@level{#1}#2}
+\newcommand*\LHead[4]{#2\ld@fs{#1}\ld@pair{#1}{\ld@tuple@a{#1}{#3}}#4}
+\newcommand*\LRef[2]{\ld@lref{#1}#2}
+\newcommand*\LSup[3]{#2\ld@lsup{#1}{}#3}
+\newcommand*\LSupA[4]{#3\ld@lsupa{#1}{\ld@tuple@a{#1}{#2}}#4}
+\newcommand*\LSupC[4]{#3\ld@lsup{#1}{\ld@tuple@a{#1}{#2}}#4}
+\newcommand*\LSupT[4]{#3\ld@lsupt{#1}{\ld@tuple@a{#1}{#2}}#4}
+\newcommand*\LTB[5]{\ld@tuple@b{#1}{#2}{#3}\ld@lt{#1}\ld@tuple@b{#1}{#4}{#5}}
+\newcommand*\MkSH[3]{\ld@mksh{#1}\ld@tuple@b{#1}{#2}{#3}}
+\newcommand*\Next[3]{\ld@next{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\NextS[4]{\ld@next{#1}{^{#4}\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\PlusA[4]{#3\ld@plus{#1}{\ld@tuple@a{#1}{#2}}#4}
+\newcommand*\RCandidate[5]{\ld@tuple@b{#1}{#3}{#4}\ld@in{#1}\ld@rcandidate{#1}{\ld@tuple@a{#1}{#2}}#5}
+\newcommand*\RNormal[3]{#2\ld@env{#1}\ld@rnormal{#1}#3}
+\newcommand*\RStep[3]{#2\ld@rstep{#1}#3}
+\newcommand*\RStepA[4]{#2\ld@env{#1}#3\ld@rstep{#1}#4}
+\newcommand*\RStepS[3]{#2\ld@rsteps{#1}#3}
+\newcommand*\RStepSA[4]{#2\ld@env{#1}#3\ld@rsteps{#1}#4}
+\newcommand*\RStrong[3]{#2\ld@env{#1}\ld@rstrong{#1}#3}
+\newcommand*\SameTop[3]{#2\ld@sametop{#1}#3}
+\newcommand*\Shift[3]{#2\ld@shift{#1}#3}
+\newcommand*\SubEq[3]{#2\ld@subeq{#1}#3}
+\newcommand*\Subst[5]{\mathop{\ld@oB{#1}#3\ld@subst{#1}#2\ld@cB{#1}}#4\ld@eq{#1}#5}
+\newcommand*\SubstB[7]{\mathop{\ld@oB{#1}#3\ld@subst{#1}#2\ld@cB{#1}}\ld@tuple@b{#1}{#4}{#5}\ld@eq{#1}\ld@tuple@b{#1}{#6}{#7}}
+\newcommand*\SubstS[5]{\mathop{\ld@oB{#1}#3\ld@substs{#1}#2\ld@cB{#1}}#4\ld@eq{#1}#5}
+\newcommand*\SuccA[3]{\ld@succ{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\THead[4]{\ld@pair{#1}{\ld@tuple@a{#1}{#2}}#3\ld@fs{#1}#4}
+\newcommand*\To[3]{#2\ld@to{#1}#3}
+\newcommand*\TStep[5]{#3\ld@env{#1}#4\ld@tstep{#1}{\ld@tuple@a{#1}{#2}}#5}
+\newcommand*\TStepS[5]{#3\ld@env{#1}#4\ld@tsteps{#1}{\ld@tuple@a{#1}{#2}}#5}
+\newcommand*\Type[5]{#3\ld@env{#1}#4\ld@type{#1}{\ld@tuple@a{#1}{#2}}#5}
+\newcommand*\Valid[4]{\ld@valid{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
+\newcommand*\WeightA[2]{\ld@weight{#1}\ld@tuple@a{#1}{#2}}
+\newcommand*\WeightB[3]{\ld@weight{#1}\ld@tuple@b{#1}{#2}{#3}}