%\def\ifstreq#1#2{\ifEqString{#1}{#2}}

\newcommand{\impsub}{\rightslice}
\newcommand{\wellformed}{\textbf{wf}}
\newcommand{\judgewf}{\vdash}
\newcommand{\judgetyped}{\vdash}
\newcommand{\judgetypea}{\vdash_{\bullet}}
\newcommand{\judgetypei}{\vdash_{\Box}}
\newcommand{\typed}{\judgetyped}
\newcommand{\typedwf}{\judgewf}
\newcommand{\typea}{\judgetypea}
\newcommand{\typeawf}{\judgetypea}
\newcommand{\typei}{\judgetypei}
\newcommand{\typeiwf}{\judgetypei}
\newcommand{\typecci}{\vdash_{CCI}}
\newcommand{\typec}{\vdash_{CCI}}
\newcommand{\typeq}{\vdash_{?}}
\newcommand{\type}{\typed}
\newcommand{\typewf}{\typedwf}
\newcommand{\judgesubd}{\vdash}
\newcommand{\judgesuba}{\vdash_{\bullet}}
\newcommand{\judgesubi}{\vdash_{\Box}}
\newcommand{\subtd}{\judgesubd}
\newcommand{\subta}{\judgesuba}
\newcommand{\subti}{\judgesubi}
\newcommand{\subt}{\subtd}
\newcommand{\subd}{\rightslice}
\newcommand{\suba}{\rightslice_{\bullet}}
\newcommand{\subi}{\rightslice_{\Box}}
\newcommand{\sub}{\subd}

\def\judgerw{~{\mbox{$"~>"$}}~}
\newcommand{\wf}[1]{\type #1~\wellformed}

\newcommand{\mualgoprim}[1]{\mu_{\bullet}'(#1)}
\newcommand{\mualgo}[1]{\mu_{\bullet}(#1)}
\newcommand{\muimplprim}[1]{\mu_{\Box}'(#1)}
\newcommand{\muimpl}[1]{\mu_{\Box}(#1)}

\newcommand{\tcoq}[3]{#1 \typec #2 : #3}
\newcommand{\tgen}[3]{#1 \type #2 : #3}
\newcommand{\subgen}[4]{#1 \type #2 \sub #3 : #4}

\newcommand{\tgensub}[5]{#1 \type #2 : #3 \quad #1 \type #3 \sub #4 : #5}
\newcommand{\wfgen}[1]{\typewf #1 \wellformed}
\newcommand{\talgo}[3]{#1 \typea #2 : #3}
\newcommand{\talgosub}[5]{#1 \typea #2 : #3 \suba #4 : #5}
\newcommand{\tdecl}[3]{#1 \typed #2 : #3}
\newcommand{\subalgo}[4]{#1 \typea #2 \suba #3 : #4}

\newcommand{\typeafn}[2]{\typeml_{#1}(#2)}

% \def\typenv#1{\typeout{Changing to #1 version}
%   \def\typewf{\csname\string\type\string#1\string{wf}\endcsname}
%   \def\type{\csname\string\type\string#1\endcsname}
%   \def\subt{\csname\string\subt#1\endcsname}
%   \def\sub{\csname\string\sub\string#1\endcsname}
% }

\newcommand{\typenvd}{
%  \typeout{Changing to declarative version}
  %\def\typewf{\typewf}
  \def\type{\typed}
  \def\subt{\subtd}
  \def\sub{\subd}
  \def\fCenter{\type}
}

\newcommand{\typenva}{
%  \typeout{Changing to algorithmic version}
  %\def\typewf{\typewf}
  \def\type{\typea}
  \def\subt{\subta}
  \def\sub{\suba}
  \def\fCenter{\type}
}

\newcommand{\typenvi}{
%  \typeout{Changing to implementation version}
  %\def\typewf{\typewf}
  \def\type{\typei}
  \def\subt{\subti}
  \def\sub{\subi}
  \def\subhnf{\subihnf}
  \def\fCenter{\type}
}


\newcommand{\matht}[1]{\text{{\tt #1}}}

\def\even{\matht{even}}
\def\odd{\matht{odd}}

\def\WfEmptyRule{Wf-Empty}
\def\WfVarRule{Wf-Var}
\def\PropSetRule{PropSet}
\def\TypeRule{Type}
\def\VarRule{Var}
\def\ProdRule{Prod}
\def\AbsRule{Abs}
\def\AppRule{App}
\def\LetInRule{Let-In}
\def\SigmaRule{Sum}
\def\SumRule{Sum}
\def\LetSumRule{Let-Sum}
\def\PiLeftRule{Pi-1}
\def\PiRightRule{Pi-2}
\def\SumInfRule{Sum-Inf}
\def\SumDepRule{Pair}
\def\SubsetRule{Subset}
\def\LetSubRule{Let-Sub}
\def\SubsumRule{Coerce}
\def\CoerceRule{Coerce}
\def\ConvRule{Conv}

\def\SubReflRule{$\rightslice$-Refl}
\def\SubSymRule{$\rightslice$-Sym}
\def\SubTransRule{$\rightslice$-Trans} 
\def\SubConvRule{$\rightslice$-Conv}
\def\SubHnfRule{$\rightslice$-$\downarrow$}
\def\SubIdRule{$\rightslice$-Id}
\def\SubBetaRule{$\rightslice$-$\beta$}
\def\SubEqRule{$\rightslice$-Eq}
\def\SubProdRule{$\rightslice$-Prod}
\def\SubSigmaRule{$\rightslice$-Sum}
\def\SubLeftRule{$\rightslice$-Left}
\def\SubRightRule{$\rightslice$-Right}
\def\SubProofRule{$\rightslice$-Proof}
\def\SubSubRule{$\rightslice$-Subset}
\def\SubTransRule{$\rightslice$-Trans}

\def\BetaTeqRule{$\beta$-$`=$}
\def\PiLeftTeqRule{$\Pi_1$-$`=$}
\def\PiRightTeqRule{$\Pi_2$-$`=$}
\def\AppTeqRule{App-$`=$}
\def\PairTeqRule{Pair-$`=$}
\def\PiTeqRule{Prod-$`=$}
\def\SigmaTeqRule{Sigma-$`=$}
\def\SubsetTeqRule{Subset-$`=$}

\def\inductionon#1{
  \ifstreq{#1}{typing-decl}{Par induction sur la dérivation de typage.}
  {\ifstreq{#1}{typing-algo}{Par induction sur la dérivation de
      typage dans le système algorithmique.}
    {\ifstreq{#1}{typing-impl}{Par induction sur la dérivation de
        typage.}
      {\ifstreq{#1}{subtyping-decl}{Par induction sur la dérivation de
          sous-typage.}
        {\ifstreq{#1}{subtyping-algo}{Par induction sur la dérivation de
            sous-typage dans le système algorithmique.}
          {\ifstreq{#1}{subtyping-impl}{Par induction sur la dérivation de
              sous-typage.}}}}}}}

\newcounter{inductiondepth}

\newenvironment{induction}[1][text=\empty]{
  \if#1\empty\text\else\inductionon{#1}\fi
  \addtocounter{inductiondepth}{1}
  \begin{list}{Unset default item}{\setlength{\leftmargin}{35pt}}}
  {\end{list}\addtocounter{inductiondepth}{-1}}

\newcommand{\inductioncasepoint}{
  \ifthenelse{\equal{\value{inductiondepth}}{1}}%
  {--}{\ifthenelse{\equal{\value{inductiondepth}}{2}}%
    {\textbullet}{--}}}

\providecommand{\case}[1]{\item[\inductioncasepoint{}] \rulename{#1} :}
\newcommand{\casetwo}[2]{\item[\inductioncasepoint{}] \rulename{#1}, \rulename{#2} :}
\newcommand{\casenil}{\item[\inductioncasepoint{}]\xspace}
\newcommand{\caseother}[1]{\item[\inductioncasepoint{}] #1 :}

%% Should be able to work with \else...
\newcommand{\inductionrule}[1]
{\ifstreq{#1}{WfEmpty}{\WfEmptyRule}
{\ifstreq{#1}{WfVar}{\WfVarRule}
{\ifstreq{#1}{PropSet}{\PropSetRule}
{\ifstreq{#1}{Type}{\TypeRule}
{\ifstreq{#1}{Var}{\VarRule}
{\ifstreq{#1}{Prod}{\ProdRule}
{\ifstreq{#1}{Abs}{\AbsRule}
{\ifstreq{#1}{LetIn}{\LetInRule}
{\ifstreq{#1}{Sigma}{\SigmaRule}
{\ifstreq{#1}{Sum}{\SumRule}
{\ifstreq{#1}{LetSum}{\LetSumRule}
{\ifstreq{#1}{PiLeft}{\PiLeftRule}
{\ifstreq{#1}{PiRight}{\PiRightRule}
{\ifstreq{#1}{App}{\AppRule}
{\ifstreq{#1}{SumInf}{\SumInfRule}
{\ifstreq{#1}{SumDep}{\SumDepRule}
{\ifstreq{#1}{LetSub}{\LetSubRule}
{\ifstreq{#1}{Subsum}{\CoerceRule}
{\ifstreq{#1}{Coerce}{\CoerceRule}
{\ifstreq{#1}{Conv}{\ConvRule}
{\ifstreq{#1}{Subset}{\SubsetRule}
{\ifstreq{#1}{SubRefl}{\SubReflRule}
{\ifstreq{#1}{SubSym}{\SubSymRule}
{\ifstreq{#1}{SubTrans}{\SubTransRule}
{\ifstreq{#1}{SubConv}{\SubConvRule}
{\ifstreq{#1}{SubHnf}{\SubHnfRule}
{\ifstreq{#1}{SubEq}{\SubEqRule}
{\ifstreq{#1}{SubProd}{\SubProdRule}
{\ifstreq{#1}{SubSigma}{\SubSigmaRule}
{\ifstreq{#1}{SubLeft}{\SubLeftRule}
{\ifstreq{#1}{SubId}{\SubIdRule}
{\ifstreq{#1}{SubBeta}{\SubBetaRule}
{\ifstreq{#1}{SubRight}{\SubRightRule}
{\ifstreq{#1}{SubProof}{\SubProofRule}
{\ifstreq{#1}{SubSub}{\SubSubRule}
{\ifstreq{#1}{BetaTeq}{\BetaTeqRule}
{\ifstreq{#1}{PiLeftTeq}{\PiLeftTeqRule}
{\ifstreq{#1}{PiRightTeq}{\PiRightTeqRule}
{\ifstreq{#1}{AppTeq}{\AppTeqRule}
{\ifstreq{#1}{PairTeq}{\PairTeqRule}
{\ifstreq{#1}{PiTeq}{\PiTeqRule}
{\ifstreq{#1}{SigmaTeq}{\SigmaTeqRule}
{\ifstreq{#1}{SubsetTeq}{\SubsetTeqRule}
{\ifstreq{#1}{*}{\_}{#1}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
\newcommand{\rulename}[1]{{\sc \inductionrule{#1}}}

% Factorize!!!
\def\indrule{\rulename}
\def\irule{\rulename}
\def\rname{\rulename}

\def\rulelabel{\rulename}

\def\infvspace{1em}

\newcommand{\ip}[2]{\llbracket #1 \rrbracket_{#2}}
\newcommand{\ipG}[1]{\llbracket #1 \rrbracket}
\newcommand{\ipt}[2]{\llfloor #1 \rrfloor_{#2}}
\newcommand{\ipT}[2]{\llceil #1 \rrceil_{#2}}

\newcommand{\coerce}[3]{\sref{coerce}_{#1}~#2~#3}
\newcommand{\coercehnf}[3]{\hnf{\sref{coerce}}_{#1}~#2~#3}
\newcommand{\ex}[1]{?_{#1}}
\def\iG{\ipG{`G}}

\newcommand{\pair}[3]{(#2, #3)_{#1}}
\newcommand{\eltpit}{\sigma_1}
\newcommand{\eltpip}{\sigma_2}

\newcommand{\iu}{\ip{u}{\iG}}
\newcommand{\tux}{\ip{t[u/x]}{`G, `D[u/x]}}
\newcommand{\cux}{[c[\ip{u}{`G}]/x]}
\newcommand{\tcux}{\ip{t}{\ipG{`G, x : V, `D}}[c[\ip{u}{`G}]/x]}
\newcommand{\GD}{`G, x : V, `D}
\newcommand{\Gr}{`G, `D[u/x]}
\newcommand{\iGD}{\ipG{`G, x : V, `D}}
\newcommand{\iGr}{\ipG{`G, `D[u/x]}}

\newcommand{\sideconden}[1]{\text{if #1}}
\newcommand{\otherwise}{\text{otherwise}}
\newcommand{\sidecondfr}[1]{\text{si #1}}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "subset-typing"
%%% LaTeX-command: "TEXINPUTS=\"style:$TEXINPUTS\" latex"
%%% End: