% generated by Ott 0.10.14 from: tmp_test7.ott
\documentclass[11pt]{article}
\usepackage{amsmath,amssymb}
\usepackage{supertabular}
\usepackage{geometry}
\usepackage{ifthen}
\geometry{%
a4paper,
% letterpaper,
dvips,
twoside,
left=22.5mm, right=22.5mm,
top=20mm,  bottom=30mm,
}
\usepackage{color}
\begin{document}
\newcommand{\ottdrule}[4][]{{\displaystyle\frac{\begin{array}{l}#2\end{array}}{#3}\quad\ottdrulename{#4}}}
\newcommand{\ottusedrule}[1]{\[#1\]}
\newcommand{\ottpremise}[1]{ #1 \\}
\newenvironment{ottdefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]}{}
\newenvironment{ottfundefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]\begin{displaymath}\begin{array}{l}}{\end{array}\end{displaymath}}
\newcommand{\ottfunclause}[2]{ #1 \equiv #2 \\}
\newcommand{\ottnt}[1]{\mathit{#1}}
\newcommand{\ottmv}[1]{\mathit{#1}}
\newcommand{\ottkw}[1]{\mathbf{#1}}
\newcommand{\ottcom}[1]{\text{#1}}
\newcommand{\ottdrulename}[1]{\textsc{#1}}
\newcommand{\ottcomplu}[5]{\overline{#1}^{\,#2\in #3 #4 #5}}
\newcommand{\ottcompu}[3]{\overline{#1}^{\,#2<#3}}
\newcommand{\ottcomp}[2]{\overline{#1}^{\,#2}}
\newcommand{\ottgrammartabular}[1]{\begin{supertabular}{llcllllll}#1\end{supertabular}}
\newcommand{\ottmetavartabular}[1]{\begin{supertabular}{ll}#1\end{supertabular}}
\newcommand{\ottrulehead}[3]{$#1$ & & $#2$ & & & \multicolumn{2}{l}{#3}}
\newcommand{\ottprodline}[6]{& & $#1$ & $#2$ & $#3 #4$ & $#5$ & $#6$}
\newcommand{\ottinterrule}{\\[5.0mm]}
\newcommand{\ottafterlastrule}{\\}
\newcommand{\ottmetavars}{
\ottmetavartabular{
 $ \mathit{typevar} ,\, \mathit{X} $ & \multicolumn{1}{l}{\ottcom{type variable}} \\
 $ \mathit{termvar} ,\, \mathit{x} $ & \multicolumn{1}{l}{\ottcom{term variable}} \\
 $ \mathit{label} ,\, \mathit{l} ,\, \mathit{k} $ & \multicolumn{1}{l}{\ottcom{field label}} \\
 $ \ottmv{index} ,\, \ottmv{i} ,\, \ottmv{j} ,\, \ottmv{n} ,\, \ottmv{m} $ & \multicolumn{1}{l}{\ottcom{indices}} \\
}}

\newcommand{\ottT}{
\ottrulehead{\ottnt{T}  ,\ \ottnt{S}  ,\ \ottnt{U}}{::=}{\ottcom{type}}\\ 
\ottprodline{|}{\mathit{X}}{}{}{}{\ottcom{type variable}}\\ 
\ottprodline{|}{\ottkw{Top}}{}{}{}{\ottcom{maximum type}}\\ 
\ottprodline{|}{\ottnt{T} \, \rightarrow \, \ottnt{T'}}{}{}{}{\ottcom{type of functions}}\\ 
\ottprodline{|}{ \forall   \mathit{X}  \mathord{ <: }  \ottnt{T} . \,  \ottnt{T'} }{}{\textsf{bind}\; \mathit{X}\; \textsf{in}\; \ottnt{T'}}{}{\ottcom{universal type}}\\ 
\ottprodline{|}{\ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, : \, \ottnt{T_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{n}}} \, : \, \ottnt{T_{\ottmv{n}}} \, \ottkw{\}}}{}{}{}{\ottcom{record}}\\ 
\ottprodline{|}{( \, \ottnt{T} \, )} {\textsf{S}}{}{}{}\\ 
\ottprodline{|}{[ \, \mathit{X} \, \mapsto \, \ottnt{T} \, ] \, \ottnt{T'}} {\textsf{M}}{}{}{}}

\newcommand{\ottt}{
\ottrulehead{\ottnt{t}}{::=}{\ottcom{term}}\\ 
\ottprodline{|}{\mathit{x}}{}{}{}{\ottcom{variable}}\\ 
\ottprodline{|}{ \lambda  \mathit{x}  \mathord{ : }  \ottnt{T} . \,  \ottnt{t} }{}{\textsf{bind}\; \mathit{x}\; \textsf{in}\; \ottnt{t}}{}{\ottcom{abstraction}}\\ 
\ottprodline{|}{\ottnt{t} \, \ottnt{t'}}{}{}{}{\ottcom{application}}\\ 
\ottprodline{|}{ \Lambda  \mathit{X}  \mathord{ <: }  \ottnt{T} . \,  \ottnt{t} }{}{\textsf{bind}\; \mathit{X}\; \textsf{in}\; \ottnt{t}}{}{\ottcom{type abstraction}}\\ 
\ottprodline{|}{\ottnt{t} \, [ \, \ottnt{T} \, ]}{}{}{}{\ottcom{type application}}\\ 
\ottprodline{|}{\ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, \!\! = \!\! \, \ottnt{t_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{n}}} \, \!\! = \!\! \, \ottnt{t_{\ottmv{n}}} \, \ottkw{\}}}{}{}{}{\ottcom{record}}\\ 
\ottprodline{|}{\ottnt{t} \, . \, \mathit{l}}{}{}{}{\ottcom{projection}}\\ 
\ottprodline{|}{\ottkw{let} \, \ottnt{p} \, \!\! = \!\! \, \ottnt{t} \, \ottkw{in} \, \ottnt{t'}}{}{\textsf{bind}\; \textrm{b}(\ottnt{p})\; \textsf{in}\; \ottnt{t'}}{}{\ottcom{pattern binding}}\\ 
\ottprodline{|}{( \, \ottnt{t} \, )} {\textsf{S}}{}{}{}\\ 
\ottprodline{|}{[ \, \mathit{x} \, \mapsto \, \ottnt{t} \, ] \, \ottnt{t'}} {\textsf{M}}{}{}{}\\ 
\ottprodline{|}{[ \, \mathit{X} \, \mapsto \, \ottnt{T} \, ] \, \ottnt{t}} {\textsf{M}}{}{}{}\\ 
\ottprodline{|}{\sigma \, \ottnt{t}} {\textsf{M}}{}{}{}}

\newcommand{\ottp}{
\ottrulehead{\ottnt{p}}{::=}{\ottcom{pattern}}\\ 
\ottprodline{|}{\mathit{x} \, : \, \ottnt{T}}{}{\textrm{b}=\mathit{x}}{}{\ottcom{variable pattern}}\\ 
\ottprodline{|}{\ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, \!\! = \!\! \, \ottnt{p_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{n}}} \, \!\! = \!\! \, \ottnt{p_{\ottmv{n}}} \, \ottkw{\}}}{}{\textrm{b}=\textrm{b}(\ottnt{p_{{\mathrm{1}}}}..\ottnt{p_{\ottmv{n}}})}{}{\ottcom{record pattern}}}

\newcommand{\ottv}{
\ottrulehead{\ottnt{v}}{::=}{\ottcom{values}}\\ 
\ottprodline{|}{ \lambda  \mathit{x}  \mathord{ : }  \ottnt{T} . \,  \ottnt{t} }{}{\textsf{bind}\; \mathit{x}\; \textsf{in}\; \ottnt{t}}{}{\ottcom{abstraction}}\\ 
\ottprodline{|}{ \Lambda  \mathit{X}  \mathord{ <: }  \ottnt{T} . \,  \ottnt{t} }{}{\textsf{bind}\; \mathit{X}\; \textsf{in}\; \ottnt{t}}{}{\ottcom{type abstraction}}\\ 
\ottprodline{|}{\ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, \!\! = \!\! \, \ottnt{v_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{n}}} \, \!\! = \!\! \, \ottnt{v_{\ottmv{n}}} \, \ottkw{\}}}{}{}{}{\ottcom{record}}}

\newcommand{\ottG}{
\ottrulehead{\Gamma  ,\ \Delta}{::=}{\ottcom{type environment}}\\ 
\ottprodline{|}{\ottkw{empty}}{}{}{}{}\\ 
\ottprodline{|}{\Gamma \, , \, \mathit{X} \, <: \, \ottnt{T}}{}{}{}{}\\ 
\ottprodline{|}{\Gamma \, , \, \mathit{x} \, : \, \ottnt{T}}{}{}{}{}\\ 
\ottprodline{|}{\Gamma_{{\mathrm{1}}} \, , \, .. \, , \, \Gamma_{\ottmv{n}}} {\textsf{M}}{}{}{}}

\newcommand{\otts}{
\ottrulehead{\sigma}{::=}{\ottcom{multiple term substitution}}\\ 
\ottprodline{|}{[ \, \mathit{x} \, \mapsto \, \ottnt{t} \, ]}{}{}{}{}\\ 
\ottprodline{|}{\sigma_{{\mathrm{1}}} \, , \, .. \, , \, \sigma_{\ottmv{n}}}{}{}{}{}}

\newcommand{\ottterminals}{
\ottrulehead{\ottnt{terminals}}{::=}{}\\ 
\ottprodline{|}{ \lambda }{}{}{}{}\\ 
\ottprodline{|}{ \rightarrow }{}{}{}{}\\ 
\ottprodline{|}{ \Rightarrow }{}{}{}{}\\ 
\ottprodline{|}{ \vdash }{}{}{}{}\\ 
\ottprodline{|}{ \longrightarrow }{}{}{}{}\\ 
\ottprodline{|}{ \forall }{}{}{}{}\\ 
\ottprodline{|}{ <: }{}{}{}{}\\ 
\ottprodline{|}{ \mapsto }{}{}{}{}\\ 
\ottprodline{|}{ \wedge }{}{}{}{}\\ 
\ottprodline{|}{ \vee }{}{}{}{}\\ 
\ottprodline{|}{ \!\! = \!\! }{}{}{}{}}

\newcommand{\ottformula}{
\ottrulehead{\ottnt{formula}}{::=}{}\\ 
\ottprodline{|}{\ottnt{judgement}}{}{}{}{}\\ 
\ottprodline{|}{\mathit{x} \, \!\! = \!\! \, \mathit{x'}}{}{}{}{}\\ 
\ottprodline{|}{\mathit{X} \, \!\! = \!\! \, \mathit{X'}}{}{}{}{}\\ 
\ottprodline{|}{( \, \ottnt{formula} \, )}{}{}{}{}\\ 
\ottprodline{|}{ \neg  \ottnt{formula} }{}{}{}{}\\ 
\ottprodline{|}{ \forall  \ottmv{i}  \in 1 ..  \ottmv{m}  .  \ottnt{formula} }{}{}{}{}\\ 
\ottprodline{|}{ \exists  \ottmv{i}  \in 1 ..  \ottmv{m} .  \ottnt{formula} }{}{}{}{}\\ 
\ottprodline{|}{\ottnt{formula} \, \wedge \, \ottnt{formula'}}{}{}{}{}\\ 
\ottprodline{|}{\mathit{l} \, \!\! = \!\! \, \mathit{l'}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{formula_{{\mathrm{1}}}} \quad ... \quad \ottnt{formula_{\ottmv{n}}}}{}{}{}{}}

\newcommand{\ottJudgementXXin}{
\ottrulehead{\ottnt{Judgement\_in}}{::=}{}\\ 
\ottprodline{|}{ \mathit{x}  \in  \ottkw{dom} ( \Gamma ) }{}{}{}{}\\ 
\ottprodline{|}{ \mathit{X}  \in  \ottkw{dom} ( \Gamma ) }{}{}{}{}\\ 
\ottprodline{|}{ \mathit{x}   :   \ottnt{T}  \in  \Gamma }{}{}{}{}\\ 
\ottprodline{|}{ \mathit{X}   <:   \ottnt{U}  \in  \Gamma }{}{}{}{}}

\newcommand{\ottJtype}{
\ottrulehead{\ottnt{Jtype}}{::=}{}\\ 
\ottprodline{|}{\Gamma \, \vdash \, \ottkw{ok}}{}{}{}{\ottcom{type environment $\Gamma$ is well-formed}}\\ 
\ottprodline{|}{\Gamma \, \vdash \, \ottnt{T}}{}{}{}{\ottcom{type $\ottnt{T}$ is well-formed in type environment $\Gamma$}}\\ 
\ottprodline{|}{\Gamma \, \vdash \, \ottnt{S} \, <: \, \ottnt{T}}{}{}{}{\ottcom{$\ottnt{S}$ is a subtype of $\ottnt{T}$}}\\ 
\ottprodline{|}{\Gamma \, \vdash \, \ottnt{t} \, : \, \ottnt{T}}{}{}{}{\ottcom{term $\ottnt{t}$ has type $\ottnt{T}$}}\\ 
\ottprodline{|}{\vdash \, \ottnt{p} \, : \, \ottnt{T} \, \Rightarrow \, \Delta}{}{}{}{\ottcom{pattern $\ottnt{p}$ matches type $\ottnt{T}$ giving bindings $\Delta$}}}

\newcommand{\ottJop}{
\ottrulehead{\ottnt{Jop}}{::=}{}\\ 
\ottprodline{|}{\ottnt{t_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{t_{{\mathrm{2}}}}}{}{}{}{\ottcom{$\ottnt{t_{{\mathrm{1}}}}$ reduces to $\ottnt{t_{{\mathrm{2}}}}$}}\\ 
\ottprodline{|}{\ottkw{match} \, ( \, \ottnt{p} \, , \, \ottnt{v} \, ) \, \!\! = \!\! \, \sigma}{}{}{}{}}

\newcommand{\ottjudgement}{
\ottrulehead{\ottnt{judgement}}{::=}{}\\ 
\ottprodline{|}{\ottnt{Judgement\_in}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{Jtype}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{Jop}}{}{}{}{}}

\newcommand{\ottuserXXsyntax}{
\ottrulehead{\ottnt{user\_syntax}}{::=}{}\\ 
\ottprodline{|}{\mathit{typevar}}{}{}{}{}\\ 
\ottprodline{|}{\mathit{termvar}}{}{}{}{}\\ 
\ottprodline{|}{\mathit{label}}{}{}{}{}\\ 
\ottprodline{|}{\ottmv{index}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{T}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{t}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{p}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{v}}{}{}{}{}\\ 
\ottprodline{|}{\Gamma}{}{}{}{}\\ 
\ottprodline{|}{\sigma}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{terminals}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{formula}}{}{}{}{}}

\newcommand{\ottgrammar}{\ottgrammartabular{
\ottT\ottinterrule
\ottt\ottinterrule
\ottp\ottinterrule
\ottv\ottinterrule
\ottG\ottinterrule
\otts\ottinterrule
\ottterminals\ottinterrule
\ottformula\ottinterrule
\ottJudgementXXin\ottinterrule
\ottJtype\ottinterrule
\ottJop\ottinterrule
\ottjudgement\ottinterrule
\ottuserXXsyntax\ottafterlastrule
}}

% defnss
% defns Judgement_in
% defn xinG
\newcommand{\ottdrulexinGXXOne}[1]{\ottdrule[#1]{%
}{
 \mathit{x}  \in  \ottkw{dom} ( \Gamma \, , \, \mathit{x} \, : \, \ottnt{T} ) }{
{\ottdrulename{xinG\_1}}{}
}}


\newcommand{\ottdrulexinGXXTwo}[1]{\ottdrule[#1]{%
\ottpremise{ \mathit{x}  \in  \ottkw{dom} ( \Gamma ) }%
}{
 \mathit{x}  \in  \ottkw{dom} ( \Gamma \, , \, \mathit{X'} \, <: \, \ottnt{U'} ) }{
{\ottdrulename{xinG\_2}}{}
}}


\newcommand{\ottdrulexinGXXThree}[1]{\ottdrule[#1]{%
\ottpremise{ \mathit{x}  \in  \ottkw{dom} ( \Gamma ) }%
}{
 \mathit{x}  \in  \ottkw{dom} ( \Gamma \, , \, \mathit{x'} \, : \, \ottnt{T'} ) }{
{\ottdrulename{xinG\_3}}{}
}}

\newcommand{\ottdefnxinG}[1]{\begin{ottdefnblock}[#1]{$ \mathit{x}  \in  \ottkw{dom} ( \Gamma ) $}{}
\ottusedrule{\ottdrulexinGXXOne{}}
\ottusedrule{\ottdrulexinGXXTwo{}}
\ottusedrule{\ottdrulexinGXXThree{}}
\end{ottdefnblock}}


% defn XinG
\newcommand{\ottdruleXinGXXOne}[1]{\ottdrule[#1]{%
}{
 \mathit{X}  \in  \ottkw{dom} ( \Gamma \, , \, \mathit{X} \, <: \, \ottnt{U} ) }{
{\ottdrulename{XinG\_1}}{}
}}


\newcommand{\ottdruleXinGXXTwo}[1]{\ottdrule[#1]{%
\ottpremise{ \mathit{X}  \in  \ottkw{dom} ( \Gamma ) }%
}{
 \mathit{X}  \in  \ottkw{dom} ( \Gamma \, , \, \mathit{X'} \, <: \, \ottnt{U'} ) }{
{\ottdrulename{XinG\_2}}{}
}}


\newcommand{\ottdruleXinGXXThree}[1]{\ottdrule[#1]{%
\ottpremise{ \mathit{X}  \in  \ottkw{dom} ( \Gamma ) }%
}{
 \mathit{X}  \in  \ottkw{dom} ( \Gamma \, , \, \mathit{x'} \, : \, \ottnt{T'} ) }{
{\ottdrulename{XinG\_3}}{}
}}

\newcommand{\ottdefnXinG}[1]{\begin{ottdefnblock}[#1]{$ \mathit{X}  \in  \ottkw{dom} ( \Gamma ) $}{}
\ottusedrule{\ottdruleXinGXXOne{}}
\ottusedrule{\ottdruleXinGXXTwo{}}
\ottusedrule{\ottdruleXinGXXThree{}}
\end{ottdefnblock}}


% defn tin
\newcommand{\ottdruletinXXOne}[1]{\ottdrule[#1]{%
}{
 \mathit{x}   :   \ottnt{T}  \in  \Gamma \, , \, \mathit{x} \, : \, \ottnt{T} }{
{\ottdrulename{tin\_1}}{}
}}


\newcommand{\ottdruletinXXTwo}[1]{\ottdrule[#1]{%
\ottpremise{ \mathit{x}   :   \ottnt{T}  \in  \Gamma }%
}{
 \mathit{x}   :   \ottnt{T}  \in  \Gamma \, , \, \mathit{X'} \, <: \, \ottnt{U'} }{
{\ottdrulename{tin\_2}}{}
}}


\newcommand{\ottdruletinXXThree}[1]{\ottdrule[#1]{%
\ottpremise{ \mathit{x}   :   \ottnt{T}  \in  \Gamma }%
}{
 \mathit{x}   :   \ottnt{T}  \in  \Gamma \, , \, \mathit{x'} \, : \, \ottnt{T'} }{
{\ottdrulename{tin\_3}}{}
}}

\newcommand{\ottdefntin}[1]{\begin{ottdefnblock}[#1]{$ \mathit{x}   :   \ottnt{T}  \in  \Gamma $}{}
\ottusedrule{\ottdruletinXXOne{}}
\ottusedrule{\ottdruletinXXTwo{}}
\ottusedrule{\ottdruletinXXThree{}}
\end{ottdefnblock}}


% defn Tin
\newcommand{\ottdruleTinXXOne}[1]{\ottdrule[#1]{%
}{
 \mathit{X}   <:   \ottnt{U}  \in  \Gamma \, , \, \mathit{X} \, <: \, \ottnt{U} }{
{\ottdrulename{Tin\_1}}{}
}}


\newcommand{\ottdruleTinXXTwo}[1]{\ottdrule[#1]{%
\ottpremise{ \mathit{X}   <:   \ottnt{U}  \in  \Gamma }%
}{
 \mathit{X}   <:   \ottnt{U}  \in  \Gamma \, , \, \mathit{X'} \, <: \, \ottnt{U'} }{
{\ottdrulename{Tin\_2}}{}
}}


\newcommand{\ottdruleTinXXThree}[1]{\ottdrule[#1]{%
\ottpremise{ \mathit{X}   <:   \ottnt{U}  \in  \Gamma }%
}{
 \mathit{X}   <:   \ottnt{U}  \in  \Gamma \, , \, \mathit{x'} \, : \, \ottnt{T'} }{
{\ottdrulename{Tin\_3}}{}
}}

\newcommand{\ottdefnTin}[1]{\begin{ottdefnblock}[#1]{$ \mathit{X}   <:   \ottnt{U}  \in  \Gamma $}{}
\ottusedrule{\ottdruleTinXXOne{}}
\ottusedrule{\ottdruleTinXXTwo{}}
\ottusedrule{\ottdruleTinXXThree{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsJudgementXXin}{
\ottdefnxinG{}
\ottdefnXinG{}
\ottdefntin{}
\ottdefnTin{}}


% defns Jtype
% defn Gok
\newcommand{\ottdruleGokXXOne}[1]{\ottdrule[#1]{%
}{
\ottkw{empty} \, \vdash \, \ottkw{ok}}{
{\ottdrulename{Gok\_1}}{}
}}


\newcommand{\ottdruleGokXXTwo}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{T}}%
\ottpremise{ \neg  ( \,  \mathit{x}  \in  \ottkw{dom} ( \Gamma )  \, ) }%
}{
\Gamma \, , \, \mathit{x} \, : \, \ottnt{T} \, \vdash \, \ottkw{ok}}{
{\ottdrulename{Gok\_2}}{}
}}


\newcommand{\ottdruleGokXXThree}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{T}}%
\ottpremise{ \neg  ( \,  \mathit{X}  \in  \ottkw{dom} ( \Gamma )  \, ) }%
}{
\Gamma \, , \, \mathit{X} \, <: \, \ottnt{T} \, \vdash \, \ottkw{ok}}{
{\ottdrulename{Gok\_3}}{}
}}

\newcommand{\ottdefnGok}[1]{\begin{ottdefnblock}[#1]{$\Gamma \, \vdash \, \ottkw{ok}$}{\ottcom{type environment $\Gamma$ is well-formed}}
\ottusedrule{\ottdruleGokXXOne{}}
\ottusedrule{\ottdruleGokXXTwo{}}
\ottusedrule{\ottdruleGokXXThree{}}
\end{ottdefnblock}}


% defn GT
\newcommand{\ottdruleGTXXVar}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottkw{ok}}%
\ottpremise{ \mathit{X}   <:   \ottnt{U}  \in  \Gamma }%
}{
\Gamma \, \vdash \, \mathit{X}}{
{\ottdrulename{GT\_Var}}{}
}}


\newcommand{\ottdruleGTXXTop}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottkw{ok}}%
}{
\Gamma \, \vdash \, \ottkw{Top}}{
{\ottdrulename{GT\_Top}}{}
}}


\newcommand{\ottdruleGTXXFun}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{T}}%
\ottpremise{\Gamma \, \vdash \, \ottnt{T'}}%
}{
\Gamma \, \vdash \, \ottnt{T} \, \rightarrow \, \ottnt{T'}}{
{\ottdrulename{GT\_Fun}}{}
}}


\newcommand{\ottdruleGTXXForall}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, , \, \mathit{X} \, <: \, \ottnt{T} \, \vdash \, \ottnt{T'}}%
}{
\Gamma \, \vdash \,  \forall   \mathit{X}  \mathord{ <: }  \ottnt{T} . \,  \ottnt{T'} }{
{\ottdrulename{GT\_Forall}}{}
}}


\newcommand{\ottdruleGTXXRcd}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{T_{{\mathrm{1}}}} \quad .. \quad \Gamma \, \vdash \, \ottnt{T_{\ottmv{n}}}}%
}{
\Gamma \, \vdash \, \ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, : \, \ottnt{T_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{n}}} \, : \, \ottnt{T_{\ottmv{n}}} \, \ottkw{\}}}{
{\ottdrulename{GT\_Rcd}}{}
}}

\newcommand{\ottdefnGT}[1]{\begin{ottdefnblock}[#1]{$\Gamma \, \vdash \, \ottnt{T}$}{\ottcom{type $\ottnt{T}$ is well-formed in type environment $\Gamma$}}
\ottusedrule{\ottdruleGTXXVar{}}
\ottusedrule{\ottdruleGTXXTop{}}
\ottusedrule{\ottdruleGTXXFun{}}
\ottusedrule{\ottdruleGTXXForall{}}
\ottusedrule{\ottdruleGTXXRcd{}}
\end{ottdefnblock}}


% defn SA
\newcommand{\ottdruleSAXXTop}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottkw{ok}}%
}{
\Gamma \, \vdash \, \ottnt{S} \, <: \, \ottkw{Top}}{
{\ottdrulename{SA\_Top}}{}
}}


\newcommand{\ottdruleSAXXReflXXTVar}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottkw{ok}}%
}{
\Gamma \, \vdash \, \mathit{X} \, <: \, \mathit{X}}{
{\ottdrulename{SA\_Refl\_TVar}}{}
}}


\newcommand{\ottdruleSAXXTransXXTVar}[1]{\ottdrule[#1]{%
\ottpremise{ \mathit{X}   <:   \ottnt{U}  \in  \Gamma }%
\ottpremise{\Gamma \, \vdash \, \ottnt{U} \, <: \, \ottnt{T}}%
}{
\Gamma \, \vdash \, \mathit{X} \, <: \, \ottnt{T}}{
{\ottdrulename{SA\_Trans\_TVar}}{}
}}


\newcommand{\ottdruleSAXXArrow}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{T_{{\mathrm{1}}}} \, <: \, \ottnt{S_{{\mathrm{1}}}}}%
\ottpremise{\Gamma \, \vdash \, \ottnt{S_{{\mathrm{2}}}} \, <: \, \ottnt{T_{{\mathrm{2}}}}}%
}{
\Gamma \, \vdash \, \ottnt{S_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{S_{{\mathrm{2}}}} \, <: \, \ottnt{T_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{T_{{\mathrm{2}}}}}{
{\ottdrulename{SA\_Arrow}}{}
}}


\newcommand{\ottdruleSAXXAll}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{T_{{\mathrm{1}}}} \, <: \, \ottnt{S_{{\mathrm{1}}}}}%
\ottpremise{\Gamma \, , \, \mathit{X} \, <: \, \ottnt{T_{{\mathrm{1}}}} \, \vdash \, \ottnt{S_{{\mathrm{2}}}} \, <: \, \ottnt{T_{{\mathrm{2}}}}}%
}{
\Gamma \, \vdash \,  \forall   \mathit{X}  \mathord{ <: }  \ottnt{S_{{\mathrm{1}}}} . \,  \ottnt{S_{{\mathrm{2}}}}  \, <: \,  \forall   \mathit{X}  \mathord{ <: }  \ottnt{T_{{\mathrm{1}}}} . \,  \ottnt{T_{{\mathrm{2}}}} }{
{\ottdrulename{SA\_All}}{}
}}


\newcommand{\ottdruleSAXXRcd}[1]{\ottdrule[#1]{%
\ottpremise{ \forall  \ottmv{i}  \in 1 ..  \ottmv{m}  .   \exists  \ottmv{j}  \in 1 ..  \ottmv{n} .  ( \, \mathit{k_{\ottmv{i}}} \, \!\! = \!\! \, \mathit{l_{\ottmv{j}}} \, \wedge \, \Gamma \, \vdash \, \ottnt{S_{\ottmv{i}}} \, <: \, \ottnt{T_{\ottmv{j}}} \, )  }%
}{
\Gamma \, \vdash \, \ottkw{\{} \, \mathit{k_{{\mathrm{1}}}} \, : \, \ottnt{S_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{k_{\ottmv{m}}} \, : \, \ottnt{S_{\ottmv{m}}} \, \ottkw{\}} \, <: \, \ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, : \, \ottnt{T_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{n}}} \, : \, \ottnt{T_{\ottmv{n}}} \, \ottkw{\}}}{
{\ottdrulename{SA\_Rcd}}{}
}}

\newcommand{\ottdefnSA}[1]{\begin{ottdefnblock}[#1]{$\Gamma \, \vdash \, \ottnt{S} \, <: \, \ottnt{T}$}{\ottcom{$\ottnt{S}$ is a subtype of $\ottnt{T}$}}
\ottusedrule{\ottdruleSAXXTop{}}
\ottusedrule{\ottdruleSAXXReflXXTVar{}}
\ottusedrule{\ottdruleSAXXTransXXTVar{}}
\ottusedrule{\ottdruleSAXXArrow{}}
\ottusedrule{\ottdruleSAXXAll{}}
\ottusedrule{\ottdruleSAXXRcd{}}
\end{ottdefnblock}}


% defn Ty
\newcommand{\ottdruleTyXXVar}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottkw{ok}}%
\ottpremise{ \mathit{x}   :   \ottnt{T}  \in  \Gamma }%
}{
\Gamma \, \vdash \, \mathit{x} \, : \, \ottnt{T}}{
{\ottdrulename{Ty\_Var}}{}
}}


\newcommand{\ottdruleTyXXAbs}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, , \, \mathit{x} \, : \, \ottnt{T_{{\mathrm{1}}}} \, \vdash \, \ottnt{t_{{\mathrm{2}}}} \, : \, \ottnt{T_{{\mathrm{2}}}}}%
}{
\Gamma \, \vdash \,  \lambda  \mathit{x}  \mathord{ : }  \ottnt{T_{{\mathrm{1}}}} . \,  \ottnt{t_{{\mathrm{2}}}}  \, : \, \ottnt{T_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{T_{{\mathrm{2}}}}}{
{\ottdrulename{Ty\_Abs}}{}
}}


\newcommand{\ottdruleTyXXApp}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{t_{{\mathrm{1}}}} \, : \, \ottnt{T_{{\mathrm{11}}}} \, \rightarrow \, \ottnt{T_{{\mathrm{12}}}}}%
\ottpremise{\Gamma \, \vdash \, \ottnt{t_{{\mathrm{2}}}} \, : \, \ottnt{T_{{\mathrm{11}}}}}%
}{
\Gamma \, \vdash \, \ottnt{t_{{\mathrm{1}}}} \, \ottnt{t_{{\mathrm{2}}}} \, : \, \ottnt{T_{{\mathrm{12}}}}}{
{\ottdrulename{Ty\_App}}{}
}}


\newcommand{\ottdruleTyXXTAbs}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, , \, \mathit{X} \, <: \, \ottnt{T_{{\mathrm{1}}}} \, \vdash \, \ottnt{t_{{\mathrm{2}}}} \, : \, \ottnt{T_{{\mathrm{2}}}}}%
}{
\Gamma \, \vdash \,  \Lambda  \mathit{X}  \mathord{ <: }  \ottnt{T_{{\mathrm{1}}}} . \,  \ottnt{t_{{\mathrm{2}}}}  \, : \,  \forall   \mathit{X}  \mathord{ <: }  \ottnt{T_{{\mathrm{1}}}} . \,  \ottnt{T_{{\mathrm{2}}}} }{
{\ottdrulename{Ty\_TAbs}}{}
}}


\newcommand{\ottdruleTyXXTApp}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{t_{{\mathrm{1}}}} \, : \,  \forall   \mathit{X}  \mathord{ <: }  \ottnt{T_{{\mathrm{11}}}} . \,  \ottnt{T_{{\mathrm{12}}}} }%
\ottpremise{\Gamma \, \vdash \, \ottnt{T_{{\mathrm{2}}}} \, <: \, \ottnt{T_{{\mathrm{11}}}}}%
}{
\Gamma \, \vdash \, \ottnt{t_{{\mathrm{1}}}} \, [ \, \ottnt{T_{{\mathrm{2}}}} \, ] \, : \, [ \, \mathit{X} \, \mapsto \, \ottnt{T_{{\mathrm{2}}}} \, ] \, \ottnt{T_{{\mathrm{12}}}}}{
{\ottdrulename{Ty\_TApp}}{}
}}


\newcommand{\ottdruleTyXXLet}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{t_{{\mathrm{1}}}} \, : \, \ottnt{T_{{\mathrm{1}}}}}%
\ottpremise{\vdash \, \ottnt{p} \, : \, \ottnt{T_{{\mathrm{1}}}} \, \Rightarrow \, \Delta}%
\ottpremise{\Gamma \, , \, \Delta \, \vdash \, \ottnt{t_{{\mathrm{2}}}} \, : \, \ottnt{T_{{\mathrm{2}}}}}%
}{
\Gamma \, \vdash \, \ottkw{let} \, \ottnt{p} \, \!\! = \!\! \, \ottnt{t_{{\mathrm{1}}}} \, \ottkw{in} \, \ottnt{t_{{\mathrm{2}}}} \, : \, \ottnt{T_{{\mathrm{2}}}}}{
{\ottdrulename{Ty\_Let}}{}
}}


\newcommand{\ottdruleTyXXRcd}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{t_{{\mathrm{1}}}} \, : \, \ottnt{T_{{\mathrm{1}}}} \quad .. \quad \Gamma \, \vdash \, \ottnt{t_{\ottmv{n}}} \, : \, \ottnt{T_{\ottmv{n}}}}%
}{
\Gamma \, \vdash \, \ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, \!\! = \!\! \, \ottnt{t_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{n}}} \, \!\! = \!\! \, \ottnt{t_{\ottmv{n}}} \, \ottkw{\}} \, : \, \ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, : \, \ottnt{T_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{n}}} \, : \, \ottnt{T_{\ottmv{n}}} \, \ottkw{\}}}{
{\ottdrulename{Ty\_Rcd}}{}
}}


\newcommand{\ottdruleTyXXProj}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{t} \, : \, \ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, : \, \ottnt{T_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{n}}} \, : \, \ottnt{T_{\ottmv{n}}} \, \ottkw{\}}}%
}{
\Gamma \, \vdash \, \ottnt{t} \, . \, \mathit{l_{\ottmv{j}}} \, : \, \ottnt{T_{\ottmv{j}}}}{
{\ottdrulename{Ty\_Proj}}{}
}}


\newcommand{\ottdruleTyXXSub}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{t} \, : \, \ottnt{S}}%
\ottpremise{\Gamma \, \vdash \, \ottnt{S} \, <: \, \ottnt{T}}%
}{
\Gamma \, \vdash \, \ottnt{t} \, : \, \ottnt{T}}{
{\ottdrulename{Ty\_Sub}}{}
}}

\newcommand{\ottdefnTy}[1]{\begin{ottdefnblock}[#1]{$\Gamma \, \vdash \, \ottnt{t} \, : \, \ottnt{T}$}{\ottcom{term $\ottnt{t}$ has type $\ottnt{T}$}}
\ottusedrule{\ottdruleTyXXVar{}}
\ottusedrule{\ottdruleTyXXAbs{}}
\ottusedrule{\ottdruleTyXXApp{}}
\ottusedrule{\ottdruleTyXXTAbs{}}
\ottusedrule{\ottdruleTyXXTApp{}}
\ottusedrule{\ottdruleTyXXLet{}}
\ottusedrule{\ottdruleTyXXRcd{}}
\ottusedrule{\ottdruleTyXXProj{}}
\ottusedrule{\ottdruleTyXXSub{}}
\end{ottdefnblock}}


% defn Pat
\newcommand{\ottdrulePatXXVar}[1]{\ottdrule[#1]{%
}{
\vdash \, \mathit{x} \, : \, \ottnt{T} \, : \, \ottnt{T} \, \Rightarrow \, \ottkw{empty} \, , \, \mathit{x} \, : \, \ottnt{T}}{
{\ottdrulename{Pat\_Var}}{}
}}


\newcommand{\ottdrulePatXXRcd}[1]{\ottdrule[#1]{%
\ottpremise{\vdash \, \ottnt{p_{{\mathrm{1}}}} \, : \, \ottnt{T_{{\mathrm{1}}}} \, \Rightarrow \, \Delta_{{\mathrm{1}}} \quad .. \quad \vdash \, \ottnt{p_{\ottmv{n}}} \, : \, \ottnt{T_{\ottmv{n}}} \, \Rightarrow \, \Delta_{\ottmv{n}}}%
}{
\vdash \, \ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, \!\! = \!\! \, \ottnt{p_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{n}}} \, \!\! = \!\! \, \ottnt{p_{\ottmv{n}}} \, \ottkw{\}} \, : \, \ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, : \, \ottnt{T_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{n}}} \, : \, \ottnt{T_{\ottmv{n}}} \, \ottkw{\}} \, \Rightarrow \, \Delta_{{\mathrm{1}}} \, , \, .. \, , \, \Delta_{\ottmv{n}}}{
{\ottdrulename{Pat\_Rcd}}{}
}}

\newcommand{\ottdefnPat}[1]{\begin{ottdefnblock}[#1]{$\vdash \, \ottnt{p} \, : \, \ottnt{T} \, \Rightarrow \, \Delta$}{\ottcom{pattern $\ottnt{p}$ matches type $\ottnt{T}$ giving bindings $\Delta$}}
\ottusedrule{\ottdrulePatXXVar{}}
\ottusedrule{\ottdrulePatXXRcd{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsJtype}{
\ottdefnGok{}
\ottdefnGT{}
\ottdefnSA{}
\ottdefnTy{}
\ottdefnPat{}}


% defns Jop
% defn reduce
\newcommand{\ottdrulereduceXXAppAbs}[1]{\ottdrule[#1]{%
}{
( \,  \lambda  \mathit{x}  \mathord{ : }  \ottnt{T_{{\mathrm{11}}}} . \,  \ottnt{t_{{\mathrm{12}}}}  \, ) \, \ottnt{v_{{\mathrm{2}}}} \, \longrightarrow \, [ \, \mathit{x} \, \mapsto \, \ottnt{v_{{\mathrm{2}}}} \, ] \, \ottnt{t_{{\mathrm{12}}}}}{
{\ottdrulename{reduce\_AppAbs}}{}
}}


\newcommand{\ottdrulereduceXXTappTabs}[1]{\ottdrule[#1]{%
}{
( \,  \Lambda  \mathit{X}  \mathord{ <: }  \ottnt{T_{{\mathrm{11}}}} . \,  \ottnt{t_{{\mathrm{12}}}}  \, ) \, [ \, \ottnt{T_{{\mathrm{2}}}} \, ] \, \longrightarrow \, [ \, \mathit{X} \, \mapsto \, \ottnt{T_{{\mathrm{2}}}} \, ] \, \ottnt{t_{{\mathrm{12}}}}}{
{\ottdrulename{reduce\_TappTabs}}{}
}}


\newcommand{\ottdrulereduceXXLetV}[1]{\ottdrule[#1]{%
\ottpremise{\ottkw{match} \, ( \, \ottnt{p} \, , \, \ottnt{v_{{\mathrm{1}}}} \, ) \, \!\! = \!\! \, \sigma}%
}{
\ottkw{let} \, \ottnt{p} \, \!\! = \!\! \, \ottnt{v_{{\mathrm{1}}}} \, \ottkw{in} \, \ottnt{t_{{\mathrm{2}}}} \, \longrightarrow \, \sigma \, \ottnt{t_{{\mathrm{2}}}}}{
{\ottdrulename{reduce\_LetV}}{}
}}


\newcommand{\ottdrulereduceXXProjRcd}[1]{\ottdrule[#1]{%
}{
\ottkw{\{} \, \mathit{l'_{{\mathrm{1}}}} \, \!\! = \!\! \, \ottnt{v_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l'_{\ottmv{n}}} \, \!\! = \!\! \, \ottnt{v_{\ottmv{n}}} \, \ottkw{\}} \, . \, \mathit{l'_{\ottmv{j}}} \, \longrightarrow \, \ottnt{v_{\ottmv{j}}}}{
{\ottdrulename{reduce\_ProjRcd}}{}
}}


\newcommand{\ottdrulereduceXXCtxXXappXXfun}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{t_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{t'_{{\mathrm{1}}}}}%
}{
\ottnt{t_{{\mathrm{1}}}} \, \ottnt{t} \, \longrightarrow \, \ottnt{t'_{{\mathrm{1}}}} \, \ottnt{t}}{
{\ottdrulename{reduce\_Ctx\_app\_fun}}{}
}}


\newcommand{\ottdrulereduceXXCtxXXappXXarg}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{t_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{t'_{{\mathrm{1}}}}}%
}{
\ottnt{v} \, \ottnt{t_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{v} \, \ottnt{t'_{{\mathrm{1}}}}}{
{\ottdrulename{reduce\_Ctx\_app\_arg}}{}
}}


\newcommand{\ottdrulereduceXXCtxXXtypeXXfun}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{t_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{t'_{{\mathrm{1}}}}}%
}{
\ottnt{t_{{\mathrm{1}}}} \, [ \, \ottnt{T} \, ] \, \longrightarrow \, \ottnt{t'_{{\mathrm{1}}}} \, [ \, \ottnt{T} \, ]}{
{\ottdrulename{reduce\_Ctx\_type\_fun}}{}
}}


\newcommand{\ottdrulereduceXXCtxXXrecord}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{t} \, \longrightarrow \, \ottnt{t'}}%
}{
\ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, \!\! = \!\! \, \ottnt{v_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{m}}} \, \!\! = \!\! \, \ottnt{v_{\ottmv{m}}} \, , \, \mathit{l} \, \!\! = \!\! \, \ottnt{t} \, , \, \mathit{l'_{{\mathrm{1}}}} \, \!\! = \!\! \, \ottnt{t'_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l'_{\ottmv{n}}} \, \!\! = \!\! \, \ottnt{t'_{\ottmv{n}}} \, \ottkw{\}} \, \longrightarrow \, \ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, \!\! = \!\! \, \ottnt{v_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{m}}} \, \!\! = \!\! \, \ottnt{v_{\ottmv{m}}} \, , \, \mathit{l} \, \!\! = \!\! \, \ottnt{t'} \, , \, \mathit{l'_{{\mathrm{1}}}} \, \!\! = \!\! \, \ottnt{t'_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l'_{\ottmv{n}}} \, \!\! = \!\! \, \ottnt{t'_{\ottmv{n}}} \, \ottkw{\}}}{
{\ottdrulename{reduce\_Ctx\_record}}{}
}}


\newcommand{\ottdrulereduceXXCtxXXletXXbinding}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{t_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{t'_{{\mathrm{1}}}}}%
}{
\ottkw{let} \, \ottnt{p} \, \!\! = \!\! \, \ottnt{t_{{\mathrm{1}}}} \, \ottkw{in} \, \ottnt{t_{{\mathrm{2}}}} \, \longrightarrow \, \ottkw{let} \, \ottnt{p} \, \!\! = \!\! \, \ottnt{t'_{{\mathrm{1}}}} \, \ottkw{in} \, \ottnt{t_{{\mathrm{2}}}}}{
{\ottdrulename{reduce\_Ctx\_let\_binding}}{}
}}

\newcommand{\ottdefnreduce}[1]{\begin{ottdefnblock}[#1]{$\ottnt{t_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{t_{{\mathrm{2}}}}$}{\ottcom{$\ottnt{t_{{\mathrm{1}}}}$ reduces to $\ottnt{t_{{\mathrm{2}}}}$}}
\ottusedrule{\ottdrulereduceXXAppAbs{}}
\ottusedrule{\ottdrulereduceXXTappTabs{}}
\ottusedrule{\ottdrulereduceXXLetV{}}
\ottusedrule{\ottdrulereduceXXProjRcd{}}
\ottusedrule{\ottdrulereduceXXCtxXXappXXfun{}}
\ottusedrule{\ottdrulereduceXXCtxXXappXXarg{}}
\ottusedrule{\ottdrulereduceXXCtxXXtypeXXfun{}}
\ottusedrule{\ottdrulereduceXXCtxXXrecord{}}
\ottusedrule{\ottdrulereduceXXCtxXXletXXbinding{}}
\end{ottdefnblock}}


% defn M
\newcommand{\ottdruleMXXVar}[1]{\ottdrule[#1]{%
}{
\ottkw{match} \, ( \, \mathit{x} \, : \, \ottnt{T} \, , \, \ottnt{v} \, ) \, \!\! = \!\! \, [ \, \mathit{x} \, \mapsto \, \ottnt{v} \, ]}{
{\ottdrulename{M\_Var}}{}
}}


\newcommand{\ottdruleMXXRcd}[1]{\ottdrule[#1]{%
\ottpremise{ \forall  \ottmv{i}  \in 1 ..  \ottmv{m}  .   \exists  \ottmv{j}  \in 1 ..  \ottmv{n} .  ( \, \mathit{l_{\ottmv{i}}} \, \!\! = \!\! \, \mathit{k_{\ottmv{j}}} \, \wedge \, \ottkw{match} \, ( \, \ottnt{p_{\ottmv{i}}} \, , \, \ottnt{v_{\ottmv{j}}} \, ) \, \!\! = \!\! \, \sigma_{\ottmv{i}} \, )  }%
}{
\ottkw{match} \, ( \, \ottkw{\{} \, \mathit{l_{{\mathrm{1}}}} \, \!\! = \!\! \, \ottnt{p_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{l_{\ottmv{m}}} \, \!\! = \!\! \, \ottnt{p_{\ottmv{m}}} \, \ottkw{\}} \, , \, \ottkw{\{} \, \mathit{k_{{\mathrm{1}}}} \, \!\! = \!\! \, \ottnt{v_{{\mathrm{1}}}} \, , \, .. \, , \, \mathit{k_{\ottmv{n}}} \, \!\! = \!\! \, \ottnt{v_{\ottmv{n}}} \, \ottkw{\}} \, ) \, \!\! = \!\! \, \sigma_{{\mathrm{1}}} \, , \, .. \, , \, \sigma_{\ottmv{m}}}{
{\ottdrulename{M\_Rcd}}{}
}}

\newcommand{\ottdefnM}[1]{\begin{ottdefnblock}[#1]{$\ottkw{match} \, ( \, \ottnt{p} \, , \, \ottnt{v} \, ) \, \!\! = \!\! \, \sigma$}{}
\ottusedrule{\ottdruleMXXVar{}}
\ottusedrule{\ottdruleMXXRcd{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsJop}{
\ottdefnreduce{}
\ottdefnM{}}

\newcommand{\ottdefnss}{
\ottdefnsJudgementXXin
\ottdefnsJtype
\ottdefnsJop}

\newcommand{\ottall}{\ottmetavars\\[0pt]
\ottgrammar\\[5.0mm]
\ottdefnss
}

\ottall
\begin{verbatim}
Definition rules:        48 good    0 bad
Definition rule clauses: 99 good    0 bad
\end{verbatim}
\end{document}
