%===================================
% Style of the document
%===================================
%\newtheorem{example}{Example}[section]
%\newtheorem{exercise}{Exercise}[section]


\newcommand{\comentario}[1]{\texttt{#1}}

%===================================
% Keywords
%===================================

\newcommand{\Prop}{\texttt{Prop}}
\newcommand{\Set}{\texttt{Set}}
\newcommand{\Type}{\texttt{Type}}
\newcommand{\true}{\texttt{true}}
\newcommand{\false}{\texttt{false}}
\newcommand{\Lth}{\texttt{Lth}}

\newcommand{\Nat}{\texttt{nat}}
\newcommand{\nat}{\texttt{nat}}
\newcommand{\Z}  {\texttt{O}}
\newcommand{\SUCC}{\texttt{S}}
\newcommand{\pred}{\texttt{pred}}

\newcommand{\False}{\texttt{False}}
\newcommand{\True}{\texttt{True}}
\newcommand{\I}{\texttt{I}}

\newcommand{\natind}{\texttt{nat\_ind}}
\newcommand{\natrec}{\texttt{nat\_rec}}
\newcommand{\natrect}{\texttt{nat\_rect}}

\newcommand{\eqT}{\texttt{eqT}}
\newcommand{\identityT}{\texttt{identityT}}

\newcommand{\map}{\texttt{map}}
\newcommand{\iterates}{\texttt{iterates}}


%===================================
% Numbering
%===================================


\newtheorem{definition}{Definition}[section]
\newtheorem{example}{Example}[section]


%===================================
% Judgements 
%===================================


\newcommand{\JM}[2]{\ensuremath{#1 : #2}}

%===================================
% Expressions 
%===================================

\newcommand{\Case}[3][]{\ensuremath{#1\textsf{Case}~#2~\textsf of}~#3~\textsf{end}}

%=======================================

\newcommand{\snreglados} [3] {\begin{tabular}{c} \ensuremath{#1} \\[2pt]
   \ensuremath{#2}\\ \hline  \ensuremath{#3}  \end{tabular}}


\newcommand{\snregla} [2] {\begin{tabular}{c}
   \ensuremath{#1}\\ \hline  \ensuremath{#2}  \end{tabular}}


%=======================================