40 \newcommand\hflataux[1]{\llparenthesis #1 \rrparenthesis_*'}

    40 \newcommand\hflataux[1]{\llparenthesis #1 \rrparenthesis_*'}

    41 \newcommand\createdByStar[1]{\textit{createdByStar}(#1)}

    41 \newcommand\createdByStar[1]{\textit{createdByStar}(#1)}

    42 

    42 

    43 \newcommand\myequiv{\mathrel{\stackrel{\makebox[0pt]{\mbox{\normalfont\tiny equiv}}}{=}}}

    43 \newcommand\myequiv{\mathrel{\stackrel{\makebox[0pt]{\mbox{\normalfont\tiny equiv}}}{=}}}

    44 

    44 

    45 \def\case{\textit{case}}

    47 \def\case{\textit{case}}

    46 \def\sequal{\stackrel{\mbox{\scriptsize rsimp}}{=}}

    48 \def\sequal{\stackrel{\mbox{\scriptsize rsimp}}{=}}

    47 \def\rsimpalts{\textit{rsimp}_{ALTS}}

    49 \def\rsimpalts{\textit{rsimp}_{ALTS}}

    48 \def\good{\textit{good}}

    50 \def\good{\textit{good}}

    49 \def\btrue{\textit{true}}

    51 \def\btrue{\textit{true}}