\def\constant{constant}

\newcommand{\termgrammar}
{$\begin{array}{lcl}
    `a & \Coloneqq & x \\
    & | & \lambda x : `t "=>" `a \\
    & | & `a~`a \\ 
    & | & `a~`t \\
%    & | & \text{\emph{\constant}} \\
% & | & (`a,~`a) \\
    & | & \pair{\Sigma x : `t.`t}{`a}{`a} \\
%    & | & \letml~x = `a ~\inml~`a \\
    & | & \pi_1~`a `| \pi_2~`a

%    & | & \ifml~`a~\thenml~`a~\elseml~`a
  \end{array}$}

\newcommand{\typegrammarOrig}
{$\begin{array}{lcl}
    `t & \Coloneqq & x \\
    & | & `t "->" `t \\
    & | & `t~`t \\
    & | & \text{\emph{\constant}} \\
    & | & `t * `t \\
    & | & \Sigma x : `t. `t \\
    & | & \lambda x : s "=>" `t \\
    & | & `t~`a \\
    & | & \Pi x : `t. `t \\
    & | & \mysubset{x}{`t}{`t}
  \end{array}$}

\newcommand{\typegrammar}
{$\begin{array}{lcl}
    `t & \Coloneqq & x \\
    & | & `t~`t \\
    & | & `t~`a \\
    & | & \lambda x : `t "=>" `t \\
    & | & \Pi x : `t. `t \\
    & | & \Sigma x : `t. `t \\
%    & | & `t * `t \\
    & | & \mysubset{x}{`t}{`t} \\
    & | & \Set \\
    & | & \Prop \\
    & | & \Type
%    & | & \text{\emph{\constant}} 
%    & & \\
%    \text{{\tt Inductive}} & \Coloneqq & ident
  \end{array}$}