\newcommand{\WfEmptyFull}[1]{
  \UAX{WfEmpty}
  {\quad}
  {$\wf{[]}$}
  {}
}  
\newcommand{\WfEmpty}[1][\Gamma]{\WfEmptyFull{#1}}
  
\newcommand{\WfVarFull}[4]{
  \UAX{WfVar}
  {$\tgen{#1}{#2}{#3}$}
  {$\wf{#1, #4 : #2}$}
  {$#3 `: \mathcal{S}, #4 `; #1$}
}
\newcommand{\WfVar}[1][\Gamma]{\WfVarFull{#1}{A}{s}{x}}

\newcommand{\PropSetFull}[3]{
  \UAX{Axiom}
  {$\wf{#1}$}
  {$\tgen{#1}{#2}{#3}$}
  {$(#2, #3) `: \mathcal{A}$} 
}
\newcommand{\PropSet}[1][\Gamma]{\PropSetFull{#1}{s_1}{s_2}}

\newcommand{\PropTypeFull}[1]{
  \UAX{Prop}
  {$\wf{#1}$}
  {$\tgen{#1}{\Prop}{\Type}$}
  {}
}
\newcommand{\PropType}[1][\Gamma]{\PropTypeFull{#1}}

\newcommand{\PropTypeoneFull}[1]{
  \UAX{Prop}
  {$\wf{#1}$}
  {$\tgen{#1}{\Prop}{\Type(1)}$}
  {}
}
\newcommand{\PropTypeone}[1][\Gamma]{\PropTypeoneFull{#1}}

\newcommand{\SetTypeFull}[1]{
  \UAX{Set}
  {$\wf{#1}$}
  {$\tgen{#1}{\Set}{\Type}$}
  {}
}

\newcommand{\SetType}[1][\Gamma]{\SetTypeFull{#1}}

\newcommand{\TypeTypeFull}[1]{
  \UAX{Type}
  {$\wf{#1}$}
  {$\tgen{#1}{\Type(i)}{\Type(i + 1)}$}
  {$i `: `N$}
}
\newcommand{\TypeType}[1][\Gamma]{\TypeTypeFull{#1}}

\newcommand{\VarFull}[3]{
  \BAX{Var}
  {$\wf{#1}$}
  {$#2 : #3 `: #1$}
  {$\tgen{#1}{#2}{#3}$}
  {}
}
\newcommand{\Var}[1][\Gamma]{\VarFull{#1}{x}{A}} 

\newcommand{\ProdFull}[7]{
  \BAX{Prod}
  {$\tgen{#1}{#2}{#3}$}
  {$\tgen{#1, #4 : #2}{#5}{#6}$}
  {$\tgen{#1}{\Pi #4 : #2.#5}{#6}$}
   {}  %{$(#3, #6, #7) `: \mathcal{R}$} % `^{} #4 `; #1$}
}
\newcommand{\Prod}[1][\Gamma]{\ProdFull{#1}{T}{s_1}{x}{U}{s_2}{s_3}}

\newcommand{\ProdTypeFull}[7]{
  \BAX{Prod}
  {$\tgen{#1}{#2}{#3}$}
  {$\tgen{#1, #4 : #2}{#5}{#6}$}
  {$\tgen{#1}{\Pi #4 : #2.#5}{#7}$}
  {$(#3, #6, #7) `: \mathcal{R}$} % `^{} #4 `; #1$}
}
\newcommand{\ProdType}[1][\Gamma]{\ProdTypeFull{#1}{T}{s_1}{x}{U}{s_2}{s_3}}

\newcommand{\AbsFull}[6]{
  \BAX{Abs}
  {$\tgen{#1, #2 : #3}{#6}{#4}$}
  {$\tgen{#1}{\Pi #2 : #3.#4}{#5}$}
  {$\tgen{#1}{\lambda #2 : #3. #6}{\Pi #2 : #3.#4}$}
  {} %$#2 `; #1$}
}

\newcommand{\Abs}[1][\Gamma]{\AbsFull{#1}{x}{T}{U}{s}{M}}

 \newcommand{\AppFull}[6]{
  \BAX{App}
  {$\tgen{#1}{#2}{\Pi #3 : #4. #5}$}
  {$\tgen{#1}{#6}{#4}$}
  {$\tgen{#1}{(#2 #6)}{#5 [ #6 / #3 ]}$}
  {$$}
}

\newcommand{\App}[1][\Gamma]{\AppFull{#1}{f}{x}{V}{W}{u}}

\newcommand{\ConvFull}[5]{
  \BAX{Conv}
  {$\tgen{#1}{#4}{#5}$}
%  {$\tgen{#1}{#2}{#3}$}
  {$#1 \seq #5 `= #2 : #3$} % #1 \subt 
  {$\tgen{#1}{#4}{#2}$}
  {}
}
\newcommand{\Conv}[1][\Gamma]{\ConvFull{#1}{T}{s}{t}{U}} 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: