+\newcommand*\ma@tmp{}
+\newcommand*\ma@last[4]{#4}
+\newcommand*\ma@list[5]{\def\ma@tmp{#5}%
+ \ifx\ma@tmp\empty\let\ma@tmp=\ma@last\else #1#2{#5}\let\ma@tmp=\ma@list\fi
+ \ma@tmp{#3}{#2}{#3}{#4}%
+}
+\newcommand*\ma@arg[1]{#1}
+\newcommand*\ma@args{\ma@op\ma@list\relax\ma@arg\ma@cm\ma@cp}
+\newcommand*\ma@cases{\ma@list\relax\ma@arg\ma@or\relax}
+\newcommand*\ma@bind{\ma@thop{}}
+\newcommand*\ma@skip[1]{}
+
+\newcommand*\PROP{\mathord\ma@sort{PROP}}
+\newcommand*\CROP[1]{\mathord\ma@sort{CROP}}
+\newcommand*\TYPE[1]{\mathord\ma@sort{TYPE}}
+\newcommand*\LREF[2]{\ma@setoptlink{\ma@lref{#1}}{#2}}
+\newcommand*\GREF[2]{\ma@setoptlink{\ma@gref{#1}}{#2}}
+\newcommand*\ABBR[4]{\ma@op\ma@setopttarget{\ma@lref{#1}}{#2}\ma@abbr #4\ma@cast #3\ma@cp\ma@bind}
+\newcommand*\ABST[3]{\ma@op\ma@setopttarget{\ma@lref{#1}}{#2}\ma@cast #3\ma@cp\ma@bind}
+\newcommand*\PROD[3]{\def\ma@tmp{#2}%
+ \ifx\ma@tmp\empty #3\ma@arrw\else
+ \ma@op\ma@prod\ma@setopttarget{\ma@lref{#1}}{#2}\ma@cast #3\ma@cp\ma@bind\fi
+}
+\newcommand*\FALL[3]{\def\ma@tmp{#2}%
+ \ifx\ma@tmp\empty #3\ma@impl\else
+ \ma@op\ma@fall\ma@setopttarget{\ma@lref{#1}}{#2}\ma@cast #3\ma@cp\ma@bind\fi
+}
+\newcommand*\APPL[1]{#1\ma@args}
+\newcommand*\CASE[3]{#3\ma@case\ma@cases}
+\newcommand*\CAZE[3]{#3\ma@caze\ma@op\ma@qm\ma@cast #2\ma@cp\ma@cases}
+\newcommand*\PAIR[2]{#1\ma@pair #2}
+
+\newcommand*\ma@term[1]{$#1$}
+\newcommand*\ma@with{ with }
+\newcommand*\ma@comma{, }
+\newcommand*\ma@stop{.\end{ma@step}}
+\newcommand*\ma@head[6]{\def\ma@tmp{#5}%
+ \ifx\ma@tmp\empty\begin{ma@step}{#1}$\ma@setopttarget{\ma@decl{#2}}{#3}$%
+ \else\begin{ma@step}{#4}$\ma@setopttarget{\ma@decl{#5}}{#6}$%
+ \fi
+}
+\newcommand*\ma@tail{\ma@list\ma@with\ma@term\ma@comma\ma@stop}
+\newcommand*\ma@type[1]{\def\ma@tmp{#1}%
+ \ifx\ma@tmp\empty\ma@gref{(omitted)}\else #1\fi
+}
+
+\newcommand*\EXIT[1]{\ma@head{\ma@exit}{end}{}{}{}{} of block #1\ma@stop}
+\newcommand*\OPEN[3]{\ma@head{}{}{}{\ma@open}{#1}{#2} is this block #3\ma@stop}
+\newcommand*\PRIM[3]{\ma@head{}{}{}{\ma@prim}{#1}{#2} will have type: $\ma@type{#3}$\ma@stop}
+\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has type: $\ma@type{#3}$\par}
+\newcommand*\BODY[1]{being $#1$\ma@stop}
+\newcommand*\STEP[1]{by $#1$\ma@tail}
+\newcommand*\DEST[1]{by cases on $#1$\ma@tail}