\rulerCmdDef{rules.C.chr.base.scheme}{%
\ensuremath{| Red ^^^  ^^^ x (sub ( ~> ) (coe')) y | }
}
\rulerCmdDef{rules.C.chr.base.a.sym}{%
\rulerRule{a.sym}{C}
{%
| (sub (Ass) (x)) ^^^  ^^^ ty | ^{ | a | } |  =*= ty | ^{ | b | } |  (brack (sc)) | 
}
{%
| (sub (Ass) (y)) ^^^  ^^^ ty | ^{ | b | } |  =*= ty | ^{ | a | } |  (brack (sc)) | 
\\
| Red ^^^  ^^^ x (sub ( ~> ) (( \ coe dot sym coe))) y | 
}
}

\rulerCmdDef{rules.C.chr.base.a.trans}{%
\rulerRule{a.trans}{C}
{%
| (sub (Ass) (x)) ^^^  ^^^ ty | ^{ | a | } |  =*= ty | ^{ | b | } |  (brack (sc1)) | 
\\
| (sub (Ass) (y)) ^^^  ^^^ ty | ^{ | b | } |  =*= ty | ^{ | c | } |  (brack (sc2)) | 
\\
| (sc1 sc2) `visible` sc3 | 
}
{%
| (sub (Ass) (z)) ^^^  ^^^ ty | ^{ | a | } |  =*= ty | ^{ | c | } |  (brack (sc3)) | 
\\
| Red ^^^  ^^^ x , y (sub ( ~> ) (transcoe)) z | 
}
}

\rulerCmdDef{rules.C.chr.base.a.congr}{%
\rulerRule{a.congr}{C}
{%
| (sub (Ass) (x)) ^^^  ^^^ ty | ^{ | a | } |  =*= ty | ^{ | b | } |  (brack (sc)) | 
\\
| (substitution , (overline p) , _ , coe') = Uni ty | ^{ | a | } |  ty | ^{ | b | } |  | 
}
{%
| (sub (Ass) (y)) ^^^  ^^^ (substitution (overline p)) (brack (sc)) | 
\\
| Red ^^^  ^^^ x (sub ( ~> ) (coe')) y | 
}
}

\rulerCmdDef{rules.C.chr.base.p.sym}{%
\rulerRule{p.sym}{C}
{%
| (sub (Prv) (x)) ^^^  ^^^ ty | ^{ | a | } |  =*= ty | ^{ | b | } |  (brack (sc)) | 
}
{%
| (sub (Prv) (y)) ^^^  ^^^ ty | ^{ | b | } |  =*= ty | ^{ | a | } |  (brack (sc)) | 
\\
| Red ^^^  ^^^ x (sub ( ~> ) (( \ coe dot sym coe))) y | 
}
}

\rulerCmdDef{rules.C.chr.base.p.trans}{%
\rulerRule{p.trans}{C}
{%
| (sub (Ass) (y)) ^^^  ^^^ ty | ^{ | b | } |  =*= ty | ^{ | c | } |  (brack (sc2)) | 
\\
| (sub (Prv) (x)) ^^^  ^^^ ty | ^{ | a | } |  =*= ty | ^{ | b | } |  (brack (sc1)) | 
\\
| sc2 `visible` sc1 | 
}
{%
| (sub (Prv) (z)) ^^^  ^^^ ty | ^{ | a | } |  =*= ty | ^{ | c | } |  (brack (sc1)) | 
\\
| Red ^^^  ^^^ x , y (sub ( ~> ) (transcoe)) z | 
}
}

\rulerCmdDef{rules.C.chr.base.p.congr}{%
\rulerRule{p.congr}{C}
{%
| (substitution , (overline p) , (overline coe') , _) = Uni ty | ^{ | a | } |  ty | ^{ | b | } |  | 
\\
| (sub (Prv) (x)) ^^^  ^^^ ty | ^{ | a | } |  =*= ty | ^{ | b | } |  (brack (sc)) | 
}
{%
| (sub (Prv) (y)) ^^^  ^^^ (substitution (overline p)) (brack (sc)) | 
\\
| Red ^^^  ^^^ x (sub ( ~> ) (overline coe')) y | 
}
}

\rulerCmdDef{rules.C.chr.base.p.assume}{%
\rulerRule{p.assume}{C}
{%
| (sub (Ass) (y)) ^^^  ^^^ ty | ^{ | a | } |  =*= ty | _{ | b | } |  (brack (sc2)) | 
\\
| (sub (Prv) (x)) ^^^  ^^^ ty | ^{ | a | } |  =*= ty | _{ | b | } |  (brack (sc1)) | 
\\
| sc2 `visible` sc1 | 
}
{%
| Red ^^^  ^^^ x (sub ( ~> ) ((lookup x))) y | 
}
}

\rulerCmdDef{rules.C.chr.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.C.chr.base.scheme}}{Entailment expressed with CHRs}{rules.C.chr.base}{C}
\rulerCmdUse{rules.C.chr.base.a.sym}
\hspace{1ex}
\rulerCmdUse{rules.C.chr.base.a.trans}
\hspace{1ex}
\rulerCmdUse{rules.C.chr.base.a.congr}
\hspace{1ex}
\rulerCmdUse{rules.C.chr.base.p.sym}
\hspace{1ex}
\rulerCmdUse{rules.C.chr.base.p.trans}
\hspace{1ex}
\rulerCmdUse{rules.C.chr.base.p.congr}
\hspace{1ex}
\rulerCmdUse{rules.C.chr.base.p.assume}
\end{rulerRulesetFigure}
}

\rulerCmdDef{rules.T.coercion.base.scheme}{%
\ensuremath{| env :- | _{ | c | } |  coe : ty | ^{ | a | } |  ~ ty | ^{ | b | } |  | }
}
\rulerCmdDef{rules.T.coercion.base.c.var}{%
\rulerRule{c.var}{T}
{%
| env (identx) = ty | ^{ | a | } |  ~ ty | ^{ | b | } |  | 
}
{%
| env :- | _{ | c | } |  identx : ty | ^{ | a | } |  ~ ty | ^{ | b | } |  | 
}
}

\rulerCmdDef{rules.T.coercion.base.c.app}{%
\rulerRule{c.app}{T}
{%
| env :- | _{ | c | } |  coe | ^{ | a | } |  : ty | ^{ | a | } |  ~ ty | ^{ | b | } |  | 
\\
| env :- | _{ | c | } |  coe | ^{ | f | } |  : ty | ^{ | f | } |  ~ ty | ^{ | g | } |  | 
}
{%
| env :- | _{ | c | } |  coe | ^{ | f | } |  coe | ^{ | a | } |  : ty | ^{ | f | } |  ty | ^{ | a | } |  ~ ty | ^{ | g | } |  ty | ^{ | b | } |  | 
}
}

\rulerCmdDef{rules.T.coercion.base.c.refl}{%
\rulerRule{c.refl}{T}
{%
}
{%
| env :- | _{ | c | } |  ty : ty ~ ty | 
}
}

\rulerCmdDef{rules.T.coercion.base.c.sym}{%
\rulerRule{c.sym}{T}
{%
| env :- | _{ | c | } |  coe : ty | ^{ | b | } |  ~ ty | ^{ | a | } |  | 
}
{%
| env :- | _{ | c | } |  sym coe : ty | ^{ | a | } |  ~ ty | ^{ | b | } |  | 
}
}

\rulerCmdDef{rules.T.coercion.base.c.trans}{%
\rulerRule{c.trans}{T}
{%
| env :- | _{ | c | } |  coe | ^{ | p | } |  : ty | ^{ | b | } |  ~ ty | ^{ | c | } |  | 
\\
| env :- | _{ | c | } |  coe | ^{ | q | } |  : ty | ^{ | a | } |  ~ ty | ^{ | b | } |  | 
}
{%
| env :- | _{ | c | } |  coe | ^{ | p | } |  compose coe | ^{ | q | } |  : ty | ^{ | a | } |  ~ ty | ^{ | c | } |  | 
}
}

\rulerCmdDef{rules.T.coercion.base.c.left}{%
\rulerRule{c.left}{T}
{%
| env :- | _{ | c | } |  coe : ty | ^{ | f | } |  ty | ^{ | a | } |  ~ ty | ^{ | g | } |  ty | ^{ | b | } |  | 
}
{%
| env :- | _{ | c | } |  left coe : ty | ^{ | f | } |  ~ ty | ^{ | g | } |  | 
}
}

\rulerCmdDef{rules.T.coercion.base.c.right}{%
\rulerRule{c.right}{T}
{%
| env :- | _{ | c | } |  coe : ty | ^{ | f | } |  ty | ^{ | a | } |  ~ ty | ^{ | g | } |  ty | ^{ | b | } |  | 
}
{%
| env :- | _{ | c | } |  right coe : ty | ^{ | a | } |  ~ ty | ^{ | b | } |  | 
}
}

\rulerCmdDef{rules.T.coercion.base.c.univ}{%
\rulerRule{c.univ}{T}
{%
| env :- | _{ | c | } |  coe : ty | ^{ | a | } |  ~ ty | ^{ | b | } |  | 
\\
| alpha notelem ftv (env) | 
}
{%
| env :- | _{ | c | } |  forall ^ alpha dot coe : forall ^ alpha dot ty | ^{ | a | } |  ~ forall ^ alpha dot ty | ^{ | b | } |  | 
}
}

\rulerCmdDef{rules.T.coercion.base.c.inst}{%
\rulerRule{c.inst}{T}
{%
| env :- | _{ | c | } |  coe : forall ^ alpha dot ty | ^{ | a | } |  ~ forall ^ beta dot ty | ^{ | b | } |  | 
}
{%
| env :- | _{ | c | } |  coe @ ty : (subst ty alpha) ty | ^{ | a | } |  ~ (subst ty beta) ty | ^{ | b | } |  | 
}
}

\rulerCmdDef{rules.T.coercion.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.T.coercion.base.scheme}}{Coercion type rules}{rules.T.coercion.base}{T}
\rulerCmdUse{rules.T.coercion.base.c.var}
\hspace{1ex}
\rulerCmdUse{rules.T.coercion.base.c.app}
\hspace{1ex}
\rulerCmdUse{rules.T.coercion.base.c.refl}
\hspace{1ex}
\rulerCmdUse{rules.T.coercion.base.c.sym}
\hspace{1ex}
\rulerCmdUse{rules.T.coercion.base.c.trans}
\hspace{1ex}
\rulerCmdUse{rules.T.coercion.base.c.left}
\hspace{1ex}
\rulerCmdUse{rules.T.coercion.base.c.right}
\hspace{1ex}
\rulerCmdUse{rules.T.coercion.base.c.univ}
\hspace{1ex}
\rulerCmdUse{rules.T.coercion.base.c.inst}
\end{rulerRulesetFigure}
}

\rulerCmdDef{rules.F.decl.base.scheme}{%
\ensuremath{| env :- | _{ | d | } |  d | }
}
\rulerCmdDef{rules.F.decl.base.adt}{%
\rulerRule{adt}{F}
{%
| env (C | _{ | i | } | ) = forall ^  | \overline{ | alpha | } |  dot ty | _{ | i , 0 | } |  -> dots -> ty | _{ | i , n | _{ | i | } |  | } |  -> D ^^^  | \overline{ | alpha | } |  | _{ | i | } |  | 
\\
| D `elem` env | 
}
{%
| env :- | _{ | d | } |  dta D ^^^  | \overline{ | alpha | } |  =  | \overline{ | C ^^^  | \overline{ | ty | } |  | } |  | 
}
}

\rulerCmdDef{rules.FE.decl.base.scheme}{%
\ensuremath{| env :- | _{ | d | } |  d | }
}
\rulerCmdDef{rules.FE.decl.base.adt}{%
\rulerRule{adt}{FE}
{%
| env (C | _{ | i | }^{ | unp | } | ) = forall ^  | \overline{ | alpha | } |  ^^^ exists  | \overline{ | beta | } |  | _{ | i | } |  ^^^ dot ty | _{ | i , 0 | } |  -> dots -> ty | _{ | i , n | _{ | i | } |  | } |  -> D ^^^  | \overline{ | alpha | } |  | _{ | i | } |  | 
\\
| env (C | _{ | i | } | ) = forall ^  | \overline{ | alpha | } |  forall ^  | \overline{ | beta | } |  | _{ | i | } |  ^^^ dot ty | _{ | i , 0 | } |  -> dots -> ty | _{ | i , n | _{ | i | } |  | } |  -> D ^^^  | \overline{ | alpha | } |  | _{ | i | } |  | 
\\
| D `elem` env | 
}
{%
| env :- | _{ | d | } |  dta D ^^^  | \overline{ | alpha | } |  =  | \overline{ | exists  | \overline{ | beta | } |  dot C ^^^  | \overline{ | ty | } |  | } |  | 
}
}

\rulerCmdDef{rules.G.decl.base.scheme}{%
\ensuremath{| env :- | _{ | d | } |  d | }
}
\rulerCmdDef{rules.G.decl.base.adt}{%
\rulerRule{adt}{G}
{%
| env (C | _{ | i | }^{ | unp | } | ) = forall ^  | \overline{ | alpha | } |  ^^^ exists  | \overline{ | beta | } |  | _{ | i | } |  ^^^ dot ( | \overline{ | x | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty | _{ | i , 0 | } |  -> dots -> ty | _{ | i , n | _{ | i | } |  | } |  -> D ^^^  | \overline{ | alpha | } |  | _{ | i | } |  | 
\\
| env (C | _{ | i | } | ) = forall ^  | \overline{ | alpha | } |  forall ^  | \overline{ | beta | } |  | _{ | i | } |  ^^^ dot ( | \overline{ | x | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty | _{ | i , 0 | } |  -> dots -> ty | _{ | i , n | _{ | i | } |  | } |  -> D ^^^  | \overline{ | alpha | } |  | _{ | i | } |  | 
\\
| D `elem` env | 
}
{%
| env :- | _{ | d | } |  dta D ^^^  | \overline{ | alpha | } |  =  | \overline{ |  || exists ^  | \overline{ | beta | } |  dot ( | \overline{ | x | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => C ^^^  | \overline{ | ty | } |  | } |  | 
}
}

\rulerCmdDef{rules.T.decl.base.scheme}{%
\ensuremath{| env :- | _{ | d | } |  d | }
}
\rulerCmdDef{rules.T.decl.base.adt}{%
\rulerRule{adt}{T}
{%
| env (C | _{ | i | }^{ | unp | } | ) = forall ^  | \overline{ | alpha | } |  ^^^ exists  | \overline{ | beta | } |  | _{ | i | } |  ^^^ dot ( | \overline{ | x | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty | _{ | i , 0 | } |  -> dots -> ty | _{ | i , n | _{ | i | } |  | } |  -> D ^^^  | \overline{ | alpha | } |  | _{ | i | } |  | 
\\
| env (C | _{ | i | } | ) = forall ^  | \overline{ | alpha | } |  forall ^  | \overline{ | beta | } |  | _{ | i | } |  ^^^ dot ( | \overline{ | x | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty | _{ | i , 0 | } |  -> dots -> ty | _{ | i , n | _{ | i | } |  | } |  -> D ^^^  | \overline{ | alpha | } |  | _{ | i | } |  | 
\\
| D `elem` env | 
}
{%
| env :- | _{ | d | } |  dta D ^^^  | \overline{ | alpha | } |  =  | \overline{ |  || exists ^  | \overline{ | beta | } |  dot ( | \overline{ | x | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => C ^^^  | \overline{ | ty | } |  | } |  | 
}
}

\rulerCmdDef{rules.F.decl.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.F.decl.base.scheme}}{Data definition type rules}{rules.F.decl.base}{F}
\rulerCmdUse{rules.F.decl.base.adt}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.FE.decl.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.FE.decl.base.scheme}}{Data definition type rules}{rules.FE.decl.base}{FE}
\rulerCmdUse{rules.FE.decl.base.adt}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.G.decl.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.G.decl.base.scheme}}{Data definition type rules}{rules.G.decl.base}{G}
\rulerCmdUse{rules.G.decl.base.adt}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.T.decl.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.T.decl.base.scheme}}{Data definition type rules}{rules.T.decl.base}{T}
\rulerCmdUse{rules.T.decl.base.adt}
\end{rulerRulesetFigure}
}

\rulerCmdDef{rules.G.entails.alt.scheme}{%
\ensuremath{| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | }
}
\rulerCmdDef{rules.G.entails.alt.e.refl}{%
\rulerRule{e.refl}{G}
{%
}
{%
| env ::- ty =*= ty | 
}
}

\rulerCmdDef{rules.G.entails.alt.e.sym}{%
\rulerRule{e.sym}{G}
{%
| env ::- ty | ^{ | r | } |  =*= ty | ^{ | l | } |  | 
}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | 
}
}

\rulerCmdDef{rules.G.entails.alt.e.trans}{%
\rulerRule{e.trans}{G}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | a | } |  | 
\\
| env ::- ty | ^{ | a | } |  =*= ty | ^{ | r | } |  | 
}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | 
}
}

\rulerCmdDef{rules.G.entails.alt.e.assume}{%
\rulerRule{e.assume}{G}
{%
| ty | ^{ | l | } |  =*= ty | ^{ | r | } |  `elem` env | 
}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | 
}
}

\rulerCmdDef{rules.G.entails.alt.e.subsume.left}{%
\rulerRule{e.subsume.left}{G}
{%
| env ::- ty | ^{ | f | } |  ty | ^{ | a | } |  =*= ty | ^{ | g | } |  ty | ^{ | b | } |  | 
}
{%
| env ::- ty | ^{ | f | } |  =*= ty | ^{ | g | } |  | 
}
}

\rulerCmdDef{rules.G.entails.alt.e.subsume.right}{%
\rulerRule{e.subsume.right}{G}
{%
| env ::- ty | ^{ | f | } |  ty | ^{ | a | } |  =*= ty | ^{ | g | } |  ty | ^{ | b | } |  | 
}
{%
| env ::- ty | ^{ | a | } |  =*= ty | ^{ | b | } |  | 
}
}

\rulerCmdDef{rules.G.entails.alt.e.congr}{%
\rulerRule{e.congr}{G}
{%
| env ::- ty | ^{ | a | } |  =*= ty | ^{ | b | } |  | 
\\
| env ::- ty | ^{ | f | } |  =*= ty | ^{ | g | } |  | 
}
{%
| env ::- ty | ^{ | f | } |  ty | ^{ | a | } |  =*= ty | ^{ | g | } |  ty | ^{ | b | } |  | 
}
}

\rulerCmdDef{rules.G.entails.alt.e.univ}{%
\rulerRule{e.univ}{G}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | 
\\
| alpha | _{ | i | } |  notelem ftv (env) | 
}
{%
| env ::- forall  | \overline{ | alpha | } |  dot ty | ^{ | l | } |  =*= forall  | \overline{ | alpha | } |  dot ty | ^{ | r | } |  | 
}
}

\rulerCmdDef{rules.G.entails.alt.e.inst}{%
\rulerRule{e.inst}{G}
{%
| env ::- forall ^ alpha ^ dot ty | ^{ | l | } |  =*= forall ^ beta ^ dot ty | ^{ | r | } |  | 
}
{%
| env ::- (subst ty alpha) ty | ^{ | l | } |  =*= (subst ty beta) ty | ^{ | r | } |  | 
}
}

\rulerCmdDef{rules.T.entails.alt.scheme}{%
\ensuremath{| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  ~> coe | }
}
\rulerCmdDef{rules.T.entails.alt.e.refl}{%
\rulerRule{e.refl}{T}
{%
}
{%
| env ::- ty =*= ty ~> ty | 
}
}

\rulerCmdDef{rules.T.entails.alt.e.sym}{%
\rulerRule{e.sym}{T}
{%
| env ::- ty | ^{ | r | } |  =*= ty | ^{ | l | } |  ~> coe | 
}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  ~> sym coe | 
}
}

\rulerCmdDef{rules.T.entails.alt.e.trans}{%
\rulerRule{e.trans}{T}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | a | } |  ~> coe | ^{ | 1 | } |  | 
\\
| env ::- ty | ^{ | a | } |  =*= ty | ^{ | r | } |  ~> coe | ^{ | 2 | } |  | 
}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  ~> coe | ^{ | 2 | } |  compose coe | ^{ | 1 | } |  | 
}
}

\rulerCmdDef{rules.T.entails.alt.e.assume}{%
\rulerRule{e.assume}{T}
{%
| env (identx) = (ty | ^{ | l | } |  =*= ty | ^{ | r | } | ) | 
}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  ~> identx | 
}
}

\rulerCmdDef{rules.T.entails.alt.e.subsume.left}{%
\rulerRule{e.subsume.left}{T}
{%
| env ::- ty | ^{ | f | } |  ty | ^{ | a | } |  =*= ty | ^{ | g | } |  ty | ^{ | b | } |  ~> coe | 
}
{%
| env ::- ty | ^{ | f | } |  =*= ty | ^{ | g | } |  ~> left coe | 
}
}

\rulerCmdDef{rules.T.entails.alt.e.subsume.right}{%
\rulerRule{e.subsume.right}{T}
{%
| env ::- ty | ^{ | f | } |  ty | ^{ | a | } |  =*= ty | ^{ | g | } |  ty | ^{ | b | } |  ~> coe | 
}
{%
| env ::- ty | ^{ | a | } |  =*= ty | ^{ | b | } |  ~> right coe | 
}
}

\rulerCmdDef{rules.T.entails.alt.e.congr}{%
\rulerRule{e.congr}{T}
{%
| env ::- ty | ^{ | a | } |  =*= ty | ^{ | b | } |  ~> coe | ^{ | a | } |  | 
\\
| env ::- ty | ^{ | f | } |  =*= ty | ^{ | g | } |  ~> coe | ^{ | f | } |  | 
}
{%
| env ::- ty | ^{ | f | } |  ty | ^{ | a | } |  =*= ty | ^{ | g | } |  ty | ^{ | b | } |  ~> coe | ^{ | f | } |  coe | ^{ | a | } |  | 
}
}

\rulerCmdDef{rules.T.entails.alt.e.univ}{%
\rulerRule{e.univ}{T}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  ~> coe | 
\\
| alpha | _{ | i | } |  notelem ftv (env) | 
}
{%
| env ::- forall  | \overline{ | alpha | } |  dot ty | ^{ | l | } |  =*= forall  | \overline{ | alpha | } |  dot ty | ^{ | r | } |  ~> forall  | \overline{ | alpha | } |  dot coe | 
}
}

\rulerCmdDef{rules.T.entails.alt.e.inst}{%
\rulerRule{e.inst}{T}
{%
| env ::- forall ^ alpha ^ dot ty | ^{ | l | } |  =*= forall ^ beta ^ dot ty | ^{ | r | } |  ~> coe | 
}
{%
| env ::- (subst ty alpha) ty | ^{ | l | } |  =*= (subst ty beta) ty | ^{ | r | } |  ~> coe @ ty | 
}
}

\rulerCmdDef{rules.G.entails.alt}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.G.entails.alt.scheme}}{Entailment rules (alt.)}{rules.G.entails.alt}{G}
\rulerCmdUse{rules.G.entails.alt.e.refl}
\hspace{1ex}
\rulerCmdUse{rules.G.entails.alt.e.sym}
\hspace{1ex}
\rulerCmdUse{rules.G.entails.alt.e.trans}
\hspace{1ex}
\rulerCmdUse{rules.G.entails.alt.e.assume}
\hspace{1ex}
\rulerCmdUse{rules.G.entails.alt.e.subsume.left}
\hspace{1ex}
\rulerCmdUse{rules.G.entails.alt.e.subsume.right}
\hspace{1ex}
\rulerCmdUse{rules.G.entails.alt.e.congr}
\hspace{1ex}
\rulerCmdUse{rules.G.entails.alt.e.univ}
\hspace{1ex}
\rulerCmdUse{rules.G.entails.alt.e.inst}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.T.entails.alt}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.T.entails.alt.scheme}}{Entailment rules (alt.)}{rules.T.entails.alt}{T}
\rulerCmdUse{rules.T.entails.alt.e.refl}
\hspace{1ex}
\rulerCmdUse{rules.T.entails.alt.e.sym}
\hspace{1ex}
\rulerCmdUse{rules.T.entails.alt.e.trans}
\hspace{1ex}
\rulerCmdUse{rules.T.entails.alt.e.assume}
\hspace{1ex}
\rulerCmdUse{rules.T.entails.alt.e.subsume.left}
\hspace{1ex}
\rulerCmdUse{rules.T.entails.alt.e.subsume.right}
\hspace{1ex}
\rulerCmdUse{rules.T.entails.alt.e.congr}
\hspace{1ex}
\rulerCmdUse{rules.T.entails.alt.e.univ}
\hspace{1ex}
\rulerCmdUse{rules.T.entails.alt.e.inst}
\end{rulerRulesetFigure}
}

\rulerCmdDef{rules.G.entails.base.scheme}{%
\ensuremath{| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | }
}
\rulerCmdDef{rules.G.entails.base.e.sym}{%
\rulerRule{e.sym}{G}
{%
| env ::- ty | ^{ | r | } |  =*= ty | ^{ | l | } |  | 
}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | 
}
}

\rulerCmdDef{rules.G.entails.base.e.trans}{%
\rulerRule{e.trans}{G}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | a | } |  | 
\\
| env ::- ty | ^{ | a | } |  =*= ty | ^{ | r | } |  | 
}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | 
}
}

\rulerCmdDef{rules.G.entails.base.e.assume}{%
\rulerRule{e.assume}{G}
{%
| ty | ^{ | l | } |  =*= ty | ^{ | r | } |  `elem` env | 
}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | 
}
}

\rulerCmdDef{rules.G.entails.base.e.congr}{%
\rulerRule{e.congr}{G}
{%
| env ::- v | _{ | i | } |  =*= ty | _{ | i | } |  | 
\\
| env ::- congrsubst ty | ^{ | a | } |  =*= ty | ^{ | b | } |  | 
}
{%
| env ::- ty | ^{ | a | } |  =*= ty | ^{ | b | } |  | 
}
}

\rulerCmdDef{rules.G.entails.base.e.subsume}{%
\rulerRule{e.subsume}{G}
{%
| env ::- ty [  | \overline{ | ty | ^{ | a | }} |  ]  =*= ty [  | \overline{ | ty | ^{ | b | }} |  ]  | 
}
{%
| env ::- ty | _{ | i | }^{ | a | } |  =*= ty | _{ | i | }^{ | b | } |  | 
}
}

\rulerCmdDef{rules.T.entails.base.scheme}{%
\ensuremath{| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  ~> coe | }
}
\rulerCmdDef{rules.T.entails.base.e.sym}{%
\rulerRule{e.sym}{T}
{%
| env ::- ty | ^{ | r | } |  =*= ty | ^{ | l | } |  ~> coe | 
}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  ~> sym coe | 
}
}

\rulerCmdDef{rules.T.entails.base.e.trans}{%
\rulerRule{e.trans}{T}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | a | } |  ~> coe | ^{ | 1 | } |  | 
\\
| env ::- ty | ^{ | a | } |  =*= ty | ^{ | r | } |  ~> coe | ^{ | 2 | } |  | 
}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  ~> coe | ^{ | 2 | } |  compose coe | ^{ | 1 | } |  | 
}
}

\rulerCmdDef{rules.T.entails.base.e.assume}{%
\rulerRule{e.assume}{T}
{%
| env (identx) = (ty | ^{ | l | } |  =*= ty | ^{ | r | } | ) | 
}
{%
| env ::- ty | ^{ | l | } |  =*= ty | ^{ | r | } |  ~> identx | 
}
}

\rulerCmdDef{rules.T.entails.base.e.congr}{%
\rulerRule{e.congr}{T}
{%
| env ::- v | _{ | i | } |  =*= ty | _{ | i | } |  ~> coe | _{ | i | } |  | 
\\
| coe = lift ^^^  | \overline{ | coe | } |  | 
\\
| env ::- congrsubst ty | ^{ | a | } |  =*= ty | ^{ | b | } |  ~> coe | ^{ | tl | } |  | 
}
{%
| env ::- ty | ^{ | a | } |  =*= ty | ^{ | b | } |  ~> coe | ^{ | tl | } |  compose coe | 
}
}

\rulerCmdDef{rules.T.entails.base.e.subsume}{%
\rulerRule{e.subsume}{T}
{%
| env ::- ty [  | \overline{ | ty | ^{ | a | }} |  ]  =*= ty [  | \overline{ | ty | ^{ | b | }} |  ]  ~> coe | 
\\
|  | \overline{ | coe | } |  = decompose ^^^ coe | 
}
{%
| env ::- ty | _{ | i | }^{ | a | } |  =*= ty | _{ | i | }^{ | b | } |  ~> coe | _{ | i | } |  | 
}
}

\rulerCmdDef{rules.G.entails.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.G.entails.base.scheme}}{Entailment rules}{rules.G.entails.base}{G}
\rulerCmdUse{rules.G.entails.base.e.sym}
\hspace{1ex}
\rulerCmdUse{rules.G.entails.base.e.trans}
\hspace{1ex}
\rulerCmdUse{rules.G.entails.base.e.assume}
\hspace{1ex}
\rulerCmdUse{rules.G.entails.base.e.congr}
\hspace{1ex}
\rulerCmdUse{rules.G.entails.base.e.subsume}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.T.entails.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.T.entails.base.scheme}}{Entailment rules}{rules.T.entails.base}{T}
\rulerCmdUse{rules.T.entails.base.e.sym}
\hspace{1ex}
\rulerCmdUse{rules.T.entails.base.e.trans}
\hspace{1ex}
\rulerCmdUse{rules.T.entails.base.e.assume}
\hspace{1ex}
\rulerCmdUse{rules.T.entails.base.e.congr}
\hspace{1ex}
\rulerCmdUse{rules.T.entails.base.e.subsume}
\end{rulerRulesetFigure}
}

\rulerCmdDef{rules.F.expr.base.scheme}{%
\ensuremath{| env :- | _{ | e | } |  e : ty | }
}
\rulerCmdDef{rules.F.expr.base.e.con}{%
\rulerRule{e.con}{F}
{%
| env (identc) = ty | 
}
{%
| env :- | _{ | e | } |  identc : ty | 
}
}

\rulerCmdDef{rules.F.expr.base.e.var}{%
\rulerRule{e.var}{F}
{%
| env (identx) = ty | 
}
{%
| env :- | _{ | e | } |  identx : ty | 
}
}

\rulerCmdDef{rules.F.expr.base.e.app.expr}{%
\rulerRule{e.app.expr}{F}
{%
| env :- | _{ | e | } |  a : ty | ^{ | a | } |  | 
\\
| env :- | _{ | e | } |  f : ty | ^{ | a | } |  -> ty | 
}
{%
| env :- | _{ | e | } |  f a : ty | 
}
}

\rulerCmdDef{rules.F.expr.base.e.app.univ}{%
\rulerRule{e.app.univ}{F}
{%
| env :- | _{ | e | } |  f : forall ^ alpha ^ dot ty | 
}
{%
| env :- | _{ | e | } |  f ty | ^{ | a | } |  : (subst tya alpha) ty | 
}
}

\rulerCmdDef{rules.F.expr.base.e.lam.abs}{%
\rulerRule{e.lam.abs}{F}
{%
| env ; envl :- | _{ | p | } |  p : ty | ^{ | a | } |  | 
\\
| envl env :- | _{ | e | } |  e : ty | 
}
{%
| env :- | _{ | e | } |   \ p dot e : ty | ^{ | a | } |  -> ty | 
}
}

\rulerCmdDef{rules.F.expr.base.e.univ.abs}{%
\rulerRule{e.univ.abs}{F}
{%
| v , env :- | _{ | e | } |  e : ty | 
}
{%
| env :- | _{ | e | } |  BigLam v dot e : forall ^ v ^ dot ty | 
}
}

\rulerCmdDef{rules.F.expr.base.e.let}{%
\rulerRule{e.let}{F}
{%
| env ; envl :- | _{ | p | } |  p | _{ | i | } |  : ty | _{ | i | } |  | 
\\
| envl env :- | _{ | e | } |  e : ty | 
\\
| envl env :- | _{ | e | } |  e | _{ | i | } |  : ty | _{ | i | } |  | 
}
{%
| env :- | _{ | e | } |  let ^^^  | \overline{ | p = e | } |  ^^^ in e : ty | 
}
}

\rulerCmdDef{rules.F.expr.base.e.case}{%
\rulerRule{e.case}{F}
{%
| env ; envl | _{ | i | } |  :- | _{ | p | } |  p | _{ | i | } |  : ty | ^{ | p | } |  | 
\\
| envl | _{ | i | } |  env :- | _{ | e | } |  e | _{ | i | } |  : ty | 
\\
| env :- | _{ | e | } |  e | ^{ | s | } |  : ty | ^{ | p | } |  | 
}
{%
| env :- | _{ | e | } |  (case e | ^{ | s | } |  ^^^ of ^^^  | \overline{ | p -> e | } | ) :: ty : ty | 
}
}

\rulerCmdDef{rules.FE.expr.base.scheme}{%
\ensuremath{| env :- | _{ | e | } |  e : ty | }
}
\rulerCmdDef{rules.FE.expr.base.e.con}{%
\rulerRule{e.con}{FE}
{%
| env (identc) = ty | 
}
{%
| env :- | _{ | e | } |  identc : ty | 
}
}

\rulerCmdDef{rules.FE.expr.base.e.var}{%
\rulerRule{e.var}{FE}
{%
| env (identx) = ty | 
}
{%
| env :- | _{ | e | } |  identx : ty | 
}
}

\rulerCmdDef{rules.FE.expr.base.e.app.expr}{%
\rulerRule{e.app.expr}{FE}
{%
| env :- | _{ | e | } |  a : ty | ^{ | a | } |  | 
\\
| env :- | _{ | e | } |  f : ty | ^{ | a | } |  -> ty | 
}
{%
| env :- | _{ | e | } |  f a : ty | 
}
}

\rulerCmdDef{rules.FE.expr.base.e.app.univ}{%
\rulerRule{e.app.univ}{FE}
{%
| env :- | _{ | e | } |  f : forall ^ alpha ^ dot ty | 
}
{%
| env :- | _{ | e | } |  f ty | ^{ | a | } |  : (subst tya alpha) ty | 
}
}

\rulerCmdDef{rules.FE.expr.base.e.lam.abs}{%
\rulerRule{e.lam.abs}{FE}
{%
| env ; envl :- | _{ | p | } |  p : ty | ^{ | a | } |  | 
\\
| envl env :- | _{ | e | } |  e : ty | 
\\
| ftv (ty) >< ftv (envl) <== ftv (env) | 
}
{%
| env :- | _{ | e | } |   \ p dot e : ty | ^{ | a | } |  -> ty | 
}
}

\rulerCmdDef{rules.FE.expr.base.e.univ.abs}{%
\rulerRule{e.univ.abs}{FE}
{%
| v , env :- | _{ | e | } |  e : ty | 
\\
| v notelem ftv (env) | 
}
{%
| env :- | _{ | e | } |  BigLam v dot e : forall ^ v ^ dot ty | 
}
}

\rulerCmdDef{rules.FE.expr.base.e.let}{%
\rulerRule{e.let}{FE}
{%
| env ; envl :- | _{ | p | } |  p | _{ | i | } |  : ty | _{ | i | } |  | 
\\
| envl env :- | _{ | e | } |  e : ty | 
\\
| envl env :- | _{ | e | } |  e | _{ | i | } |  : ty | _{ | i | } |  | 
\\
| ftv (ty) >< ftv (envl) <== ftv (env) | 
}
{%
| env :- | _{ | e | } |  let ^^^  | \overline{ | p = e | } |  ^^^ in e : ty | 
}
}

\rulerCmdDef{rules.FE.expr.base.e.case}{%
\rulerRule{e.case}{FE}
{%
| env ; envl | _{ | i | } |  :- | _{ | p | } |  p | _{ | i | } |  : ty | ^{ | p | } |  | 
\\
| envl | _{ | i | } |  env :- | _{ | e | } |  e | _{ | i | } |  : ty | 
\\
| env :- | _{ | e | } |  e | ^{ | s | } |  : ty | ^{ | p | } |  | 
\\
| ftv (ty | ^{ | p | } | ) >< ftv (envl | _{ | i | } | ) <== ftv (env) | 
}
{%
| env :- | _{ | e | } |  (case e | ^{ | s | } |  ^^^ of ^^^  | \overline{ | p -> e | } | ) :: ty : ty | 
}
}

\rulerCmdDef{rules.G.expr.base.scheme}{%
\ensuremath{| env :- | _{ | e | } |  e : ty | }
}
\rulerCmdDef{rules.G.expr.base.e.coerce}{%
\rulerRule{e.coerce}{G}
{%
| env :- | _{ | e | } |  e :  | \overline{ | subst ty v | } |  ty' | 
\\
| env ::- ty | _{ | i | } |  =*= v | _{ | i | } |  | 
}
{%
| env :- | _{ | e | } |  e : ty' | 
}
}

\rulerCmdDef{rules.G.expr.base.e.app.eqs}{%
\rulerRule{e.app.eqs}{G}
{%
| env ::- ty | _{ | i | }^{ | l | } |  =*= ty | _{ | i | }^{ | r | } |  |  \hspace{2ex} | env :- | _{ | e | } |  e : ( | \overline{ | ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty | 
}
{%
| env :- | _{ | e | } |  e : ty | 
}
}

\rulerCmdDef{rules.G.expr.base.e.con}{%
\rulerRule{e.con}{G}
{%
| env (identc) = ty | 
}
{%
| env :- | _{ | e | } |  identc : ty | 
}
}

\rulerCmdDef{rules.G.expr.base.e.var}{%
\rulerRule{e.var}{G}
{%
| env (identx) = ty | 
}
{%
| env :- | _{ | e | } |  identx : ty | 
}
}

\rulerCmdDef{rules.G.expr.base.e.app.expr}{%
\rulerRule{e.app.expr}{G}
{%
| env :- | _{ | e | } |  a : ty | ^{ | a | } |  | 
\\
| env :- | _{ | e | } |  f : ty | ^{ | a | } |  -> ty | 
}
{%
| env :- | _{ | e | } |  f a : ty | 
}
}

\rulerCmdDef{rules.G.expr.base.e.app.univ}{%
\rulerRule{e.app.univ}{G}
{%
| env :- | _{ | e | } |  f : forall ^ alpha ^ dot ty | 
}
{%
| env :- | _{ | e | } |  f ty | ^{ | a | } |  : (subst tya alpha) ty | 
}
}

\rulerCmdDef{rules.G.expr.base.e.lam.abs}{%
\rulerRule{e.lam.abs}{G}
{%
| env ; envl :- | _{ | p | } |  p : ty | ^{ | a | } |  | 
\\
| envl env :- | _{ | e | } |  e : ty | 
\\
| ftv (ty) >< ftv (envl) <== ftv (env) | 
}
{%
| env :- | _{ | e | } |   \ p dot e : ty | ^{ | a | } |  -> ty | 
}
}

\rulerCmdDef{rules.G.expr.base.e.univ.abs}{%
\rulerRule{e.univ.abs}{G}
{%
| v , env :- | _{ | e | } |  e : ty | 
\\
| v notelem ftv (env) | 
}
{%
| env :- | _{ | e | } |  BigLam v dot e : forall ^ v ^ dot ty | 
}
}

\rulerCmdDef{rules.G.expr.base.e.let}{%
\rulerRule{e.let}{G}
{%
| env ; envl :- | _{ | p | } |  p | _{ | i | } |  : ty | _{ | i | } |  | 
\\
| envl env :- | _{ | e | } |  e : ty | 
\\
| envl env :- | _{ | e | } |  e | _{ | i | } |  : ty | _{ | i | } |  | 
\\
| ftv (ty) >< ftv (envl) <== ftv (env) | 
}
{%
| env :- | _{ | e | } |  let ^^^  | \overline{ | p = e | } |  ^^^ in e : ty | 
}
}

\rulerCmdDef{rules.G.expr.base.e.case}{%
\rulerRule{e.case}{G}
{%
| env ; envl | _{ | i | } |  :- | _{ | p | } |  p | _{ | i | } |  : ty | ^{ | p | } |  | 
\\
| envl | _{ | i | } |  env :- | _{ | e | } |  e | _{ | i | } |  : ty | 
\\
| env :- | _{ | e | } |  e | ^{ | s | } |  : ty | ^{ | p | } |  | 
\\
| ftv (ty | ^{ | p | } | ) >< ftv (envl | _{ | i | } | ) <== ftv (env) | 
}
{%
| env :- | _{ | e | } |  (case e | ^{ | s | } |  ^^^ of ^^^  | \overline{ | p -> e | } | ) :: ty : ty | 
}
}

\rulerCmdDef{rules.T.expr.base.scheme}{%
\ensuremath{| env :- | _{ | e | } |  e : ty ~> e' | }
}
\rulerCmdDef{rules.T.expr.base.e.coerce}{%
\rulerRule{e.coerce}{T}
{%
| env :- | _{ | e | } |  e :  | \overline{ | subst ty v | } |  ty' ~> e' | 
\\
| env ::- ty | _{ | i | } |  =*= v | _{ | i | } |  ~> coe | _{ | i | } |  | 
\\
| coe = lift ^^^  | \overline{ | coe | } |  | 
\\
| ty' =  | \overline{ | subst ty v | } |  ty | 
}
{%
| env :- | _{ | e | } |  e : ty' ~> e' :> coe | 
}
}

\rulerCmdDef{rules.T.expr.base.e.app.eqs}{%
\rulerRule{e.app.eqs}{T}
{%
| env :- | _{ | e | } |  e : ( | \overline{ | ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty ~> e' | 
\\
| env ::- ty | _{ | i | }^{ | l | } |  =*= ty | _{ | i | }^{ | r | } |  ~> coe | 
}
{%
| env :- | _{ | e | } |  e : ty ~> e' coe | 
}
}

\rulerCmdDef{rules.T.expr.base.e.con}{%
\rulerRule{e.con}{T}
{%
| env (identc) = ty | 
}
{%
| env :- | _{ | e | } |  identc : ty ~> identc | 
}
}

\rulerCmdDef{rules.T.expr.base.e.var}{%
\rulerRule{e.var}{T}
{%
| env (identx) = ty | 
}
{%
| env :- | _{ | e | } |  identx : ty ~> identx | 
}
}

\rulerCmdDef{rules.T.expr.base.e.app.expr}{%
\rulerRule{e.app.expr}{T}
{%
| env :- | _{ | e | } |  a : ty | ^{ | a | } |  ~> a' | 
\\
| env :- | _{ | e | } |  f : ty | ^{ | a | } |  -> ty ~> f' | 
}
{%
| env :- | _{ | e | } |  f a : ty ~> f' a' | 
}
}

\rulerCmdDef{rules.T.expr.base.e.app.univ}{%
\rulerRule{e.app.univ}{T}
{%
| env :- | _{ | e | } |  f : forall ^ alpha ^ dot ty ~> f' | 
}
{%
| env :- | _{ | e | } |  f ty | ^{ | a | } |  : (subst tya alpha) ty ~> f' ty | ^{ | a | } |  | 
}
}

\rulerCmdDef{rules.T.expr.base.e.lam.abs}{%
\rulerRule{e.lam.abs}{T}
{%
| env ; envl :- | _{ | p | } |  p : ty | ^{ | a | } |  ~> p' | 
\\
| envl env :- | _{ | e | } |  e : ty ~> e' | 
\\
| ftv (ty) >< ftv (envl) <== ftv (env) | 
}
{%
| env :- | _{ | e | } |   \ p dot e : ty | ^{ | a | } |  -> ty ~>  \ p' dot e' | 
}
}

\rulerCmdDef{rules.T.expr.base.e.univ.abs}{%
\rulerRule{e.univ.abs}{T}
{%
| v , env :- | _{ | e | } |  e : ty ~> e' | 
\\
| v notelem ftv (env) | 
}
{%
| env :- | _{ | e | } |  BigLam v dot e : forall ^ v ^ dot ty ~> BigLam v dot e' | 
}
}

\rulerCmdDef{rules.T.expr.base.e.let}{%
\rulerRule{e.let}{T}
{%
| env ; envl :- | _{ | p | } |  p | _{ | i | } |  : ty | _{ | i | } |  ~> p' | _{ | i | } |  | 
\\
| envl env :- | _{ | e | } |  e : ty ~> e' | 
\\
| envl env :- | _{ | e | } |  e | _{ | i | } |  : ty | _{ | i | } |  ~> e' | _{ | i | } |  | 
\\
| ftv (ty) >< ftv (envl) <== ftv (env) | 
}
{%
| env :- | _{ | e | } |  let ^^^  | \overline{ | p = e | } |  ^^^ in e : ty ~> let ^^^  | \overline{ | p' = e' | } |  ^^^ in e' | 
}
}

\rulerCmdDef{rules.T.expr.base.e.case}{%
\rulerRule{e.case}{T}
{%
| env ; envl | _{ | i | } |  :- | _{ | p | } |  p | _{ | i | } |  : ty | _{ | i | }^{ | p | } |  ~> p' | _{ | i | } |  | 
\\
| envl | _{ | i | } |  env :- | _{ | e | } |  e | _{ | i | } |  : ty ~> e' | _{ | i | } |  | 
\\
| env :- | _{ | e | } |  e | ^{ | s | } |  : ty | ^{ | p | } |  ~> e' | 
\\
| ftv (ty | ^{ | p | } | ) >< ftv (envl | _{ | i | } | ) <== ftv (env) | 
}
{%
| env :- | _{ | e | } |  (case e | ^{ | s | } |  ^^^ of ^^^  | \overline{ | p -> e | } | ) :: ty : ty ~> case e' | ^{ | s | } |  ^^^ of ^^^  | \overline{ | p' -> e' | } |  | 
}
}

\rulerCmdDef{rules.F.expr.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.F.expr.base.scheme}}{Expression type rules}{rules.F.expr.base}{F}
\rulerCmdUse{rules.F.expr.base.e.con}
\hspace{1ex}
\rulerCmdUse{rules.F.expr.base.e.var}
\hspace{1ex}
\rulerCmdUse{rules.F.expr.base.e.app.expr}
\hspace{1ex}
\rulerCmdUse{rules.F.expr.base.e.app.univ}
\hspace{1ex}
\rulerCmdUse{rules.F.expr.base.e.lam.abs}
\hspace{1ex}
\rulerCmdUse{rules.F.expr.base.e.univ.abs}
\hspace{1ex}
\rulerCmdUse{rules.F.expr.base.e.let}
\hspace{1ex}
\rulerCmdUse{rules.F.expr.base.e.case}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.FE.expr.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.FE.expr.base.scheme}}{Expression type rules}{rules.FE.expr.base}{FE}
\rulerCmdUse{rules.FE.expr.base.e.con}
\hspace{1ex}
\rulerCmdUse{rules.FE.expr.base.e.var}
\hspace{1ex}
\rulerCmdUse{rules.FE.expr.base.e.app.expr}
\hspace{1ex}
\rulerCmdUse{rules.FE.expr.base.e.app.univ}
\hspace{1ex}
\rulerCmdUse{rules.FE.expr.base.e.lam.abs}
\hspace{1ex}
\rulerCmdUse{rules.FE.expr.base.e.univ.abs}
\hspace{1ex}
\rulerCmdUse{rules.FE.expr.base.e.let}
\hspace{1ex}
\rulerCmdUse{rules.FE.expr.base.e.case}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.G.expr.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.G.expr.base.scheme}}{Expression type rules}{rules.G.expr.base}{G}
\rulerCmdUse{rules.G.expr.base.e.coerce}
\hspace{1ex}
\rulerCmdUse{rules.G.expr.base.e.app.eqs}
\hspace{1ex}
\rulerCmdUse{rules.G.expr.base.e.con}
\hspace{1ex}
\rulerCmdUse{rules.G.expr.base.e.var}
\hspace{1ex}
\rulerCmdUse{rules.G.expr.base.e.app.expr}
\hspace{1ex}
\rulerCmdUse{rules.G.expr.base.e.app.univ}
\hspace{1ex}
\rulerCmdUse{rules.G.expr.base.e.lam.abs}
\hspace{1ex}
\rulerCmdUse{rules.G.expr.base.e.univ.abs}
\hspace{1ex}
\rulerCmdUse{rules.G.expr.base.e.let}
\hspace{1ex}
\rulerCmdUse{rules.G.expr.base.e.case}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.T.expr.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.T.expr.base.scheme}}{Expression type rules}{rules.T.expr.base}{T}
\rulerCmdUse{rules.T.expr.base.e.coerce}
\hspace{1ex}
\rulerCmdUse{rules.T.expr.base.e.app.eqs}
\hspace{1ex}
\rulerCmdUse{rules.T.expr.base.e.con}
\hspace{1ex}
\rulerCmdUse{rules.T.expr.base.e.var}
\hspace{1ex}
\rulerCmdUse{rules.T.expr.base.e.app.expr}
\hspace{1ex}
\rulerCmdUse{rules.T.expr.base.e.app.univ}
\hspace{1ex}
\rulerCmdUse{rules.T.expr.base.e.lam.abs}
\hspace{1ex}
\rulerCmdUse{rules.T.expr.base.e.univ.abs}
\hspace{1ex}
\rulerCmdUse{rules.T.expr.base.e.let}
\hspace{1ex}
\rulerCmdUse{rules.T.expr.base.e.case}
\end{rulerRulesetFigure}
}

\rulerCmdDef{rules.F.expr.syndir.scheme}{%
\ensuremath{| env :- | _{ | e | } |  e : ty | }
}
\rulerCmdDef{rules.F.expr.syndir.e.case}{%
\rulerRule{e.case}{F}
{%
| env ; env | _{ | i | } |  :- | _{ | p | } |  p | _{ | i | } |  : ty | _{ | i | }^{ | p | } |  | 
\\
| env | _{ | i | } |  env :- | _{ | e | } |  e | _{ | i | } |  : ty | 
\\
| env :- | _{ | e | } |  e | _{ | s | } |  : ty | _{ | i | }^{ | p | } |  | 
}
{%
| env :- | _{ | e | } |  (case e | _{ | s | } |  ^^^ of ^^^  | \overline{ | p -> e | } | ) :: ty : ty | 
}
}

\rulerCmdDef{rules.FE.expr.syndir.scheme}{%
\ensuremath{| env :- | _{ | e | } |  e : ty | }
}
\rulerCmdDef{rules.FE.expr.syndir.e.case}{%
\rulerRule{e.case}{FE}
{%
| env ; env | _{ | i | } |  :- | _{ | p | } |  p | _{ | i | } |  : ty | _{ | i | }^{ | p | } |  | 
\\
| env | _{ | i | } |  env :- | _{ | e | } |  e | _{ | i | } |  : ty | 
\\
| env :- | _{ | e | } |  e | _{ | s | } |  : ty | _{ | i | }^{ | p | } |  | 
\\
| ftv (ty | _{ | i | }^{ | p | } | ) >< ftv (env | _{ | i | } | ) <== ftv (env) | 
}
{%
| env :- | _{ | e | } |  (case e | _{ | s | } |  ^^^ of ^^^  | \overline{ | p -> e | } | ) :: ty : ty | 
}
}

\rulerCmdDef{rules.G.expr.syndir.scheme}{%
\ensuremath{| env :- | _{ | e | } |  e : ty | }
}
\rulerCmdDef{rules.G.expr.syndir.e.case}{%
\rulerRule{e.case}{G}
{%
| env ; env | _{ | i | } |  :- | _{ | p | } |  p | _{ | i | } |  : ty | _{ | i | }^{ | p | } |  | 
\\
| env | _{ | i | } |  env :- | _{ | e | } |  e | _{ | i | } |  : ty | 
\\
| env :- | _{ | e | } |  e | _{ | s | } |  : ty | _{ | i | }^{ | p | } |  | 
\\
| ftv (ty | _{ | i | }^{ | p | } | ) >< ftv (env | _{ | i | } | ) <== ftv (env) | 
}
{%
| env :- | _{ | e | } |  (case e | _{ | s | } |  ^^^ of ^^^  | \overline{ | p -> e | } | ) :: ty : ty | 
}
}

\rulerCmdDef{rules.T.expr.syndir.scheme}{%
\ensuremath{| env :- | _{ | e | } |  e : ty ~> e' | }
}
\rulerCmdDef{rules.T.expr.syndir.e.con}{%
\rulerRule{e.con}{T}
{%
| env (identc) = ( | \overline{ | ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty | 
\\
| env ::- ty | _{ | i | }^{ | l | } |  =*= ty | _{ | i | }^{ | r | } |  ~> coe | _{ | i | } |  | 
}
{%
| env :- | _{ | e | } |  e : ty ~> identc  | \overline{ | coe | } |  | 
}
}

\rulerCmdDef{rules.T.expr.syndir.e.case}{%
\rulerRule{e.case}{T}
{%
| env ; env | _{ | i | } |  :- | _{ | p | } |  p | _{ | i | } |  : ty | _{ | i | }^{ | p | } |  ~> p' | _{ | i | } |  | 
\\
| env | _{ | i | } |  env :- | _{ | e | } |  e | _{ | i | } |  : ty | _{ | i | } |  ~> e' | _{ | i | } |  | 
\\
| env | _{ | i | } |  env ::- ty | _{ | i | }^{ | r | } |  =*= v | _{ | i | } |  ~> coe | _{ | i | } |  | 
\\
| coe | _{ | i | } |  = decompose ^^^  | \overline{ | coe | _{ | i | }} |  | 
\\
| ty' =  | \overline{ | subst ty | ^{ | r | } |  v | } |  ty | 
}
{%
| env :- | _{ | e | } |  (case e | _{ | s | } |  ^^^ of ^^^  | \overline{ | p -> e | } | ) :: ty : ty ~> case e' | _{ | s | } |  ^^^ of ^^^  | \overline{ | p' -> e' :> coe | } |  | 
}
}

\rulerCmdDef{rules.F.expr.syndir}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.F.expr.syndir.scheme}}{Expression type rules (syn. dir.)}{rules.F.expr.syndir}{F}
\rulerCmdUse{rules.F.expr.syndir.e.case}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.FE.expr.syndir}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.FE.expr.syndir.scheme}}{Expression type rules (syn. dir.)}{rules.FE.expr.syndir}{FE}
\rulerCmdUse{rules.FE.expr.syndir.e.case}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.G.expr.syndir}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.G.expr.syndir.scheme}}{Expression type rules (syn. dir.)}{rules.G.expr.syndir}{G}
\rulerCmdUse{rules.G.expr.syndir.e.case}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.T.expr.syndir}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.T.expr.syndir.scheme}}{Expression type rules (syn. dir.)}{rules.T.expr.syndir}{T}
\rulerCmdUse{rules.T.expr.syndir.e.con}
\hspace{1ex}
\rulerCmdUse{rules.T.expr.syndir.e.case}
\end{rulerRulesetFigure}
}

\rulerCmdDef{rules.G.expr.trans.scheme}{%
\ensuremath{| env :- | _{ | e | } |  e : ty | }
}
\rulerCmdDef{rules.G.expr.trans.e.app.eqs}{%
\rulerRule{e.app.eqs}{G}
{%
| env :- | _{ | e | } |  e : ( | \overline{ | ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty | 
\\
| env ::- ty | _{ | i | }^{ | l | } |  =*= ty | _{ | i | }^{ | r | } |  | 
}
{%
| env :- | _{ | e | } |  e : ty | 
}
}

\rulerCmdDef{rules.G.expr.trans.e.coerce}{%
\rulerRule{e.coerce}{G}
{%
| env :- | _{ | e | } |  e :  | \overline{ | subst ty v | } |  ty' | 
\\
| env ::- ty | _{ | i | } |  =*= v | _{ | i | } |  | 
}
{%
| env :- | _{ | e | } |  e : ty' | 
}
}

\rulerCmdDef{rules.T.expr.trans.scheme}{%
\ensuremath{| env :- | _{ | e | } |  e : ty ~> e' | }
}
\rulerCmdDef{rules.T.expr.trans.e.app.eqs}{%
\rulerRule{e.app.eqs}{T}
{%
| env ::- ty | _{ | i | }^{ | l | } |  =*= ty | _{ | i | }^{ | r | } |  ~> coe | 
\\
| env :- | _{ | e | } |  e : ( | \overline{ | ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty ~> e' | 
}
{%
| env :- | _{ | e | } |  e : ty ~> e' coe | 
}
}

\rulerCmdDef{rules.T.expr.trans.e.coerce}{%
\rulerRule{e.coerce}{T}
{%
| env :- | _{ | e | } |  e :  | \overline{ | subst ty v | } |  ty' ~> e' | 
\\
| env ::- ty | _{ | i | } |  =*= v | _{ | i | } |  ~> coe | _{ | i | } |  | 
\\
| coe = lift ^^^  | \overline{ | coe | } |  | 
}
{%
| env :- | _{ | e | } |  e : ty' ~> e' :> coe | 
}
}

\rulerCmdDef{rules.G.expr.trans}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.G.expr.trans.scheme}}{Expression type rules}{rules.G.expr.trans}{G}
\rulerCmdUse{rules.G.expr.trans.e.app.eqs}
\hspace{1ex}
\rulerCmdUse{rules.G.expr.trans.e.coerce}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.T.expr.trans}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.T.expr.trans.scheme}}{Expression type rules}{rules.T.expr.trans}{T}
\rulerCmdUse{rules.T.expr.trans.e.app.eqs}
\hspace{1ex}
\rulerCmdUse{rules.T.expr.trans.e.coerce}
\end{rulerRulesetFigure}
}

\rulerCmdDef{rules.T.expr'.base.scheme}{%
\ensuremath{| env :- | _{ | e' | } |  e' : ty' | }
}
\rulerCmdDef{rules.T.expr'.base.e.cast}{%
\rulerRule{e.cast}{T}
{%
| env :- | _{ | e' | } |  e' : ty'' | ^{ | a | } |  | 
\\
| env :- | _{ | c | } |  coe : ty'' | ^{ | a | } |  ~ ty'' | ^{ | b | } |  | 
}
{%
| env :- | _{ | e' | } |  e' : ty'' | ^{ | b | } |  | 
}
}

\rulerCmdDef{rules.T.expr'.base.e.app.coe}{%
\rulerRule{e.app.coe}{T}
{%
| env :- | _{ | e' | } |  e' : coe -> ty'' | 
}
{%
| env :- | _{ | e' | } |  e' : ty'' | 
}
}

\rulerCmdDef{rules.T.expr'.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.T.expr'.base.scheme}}{Expression type rules}{rules.T.expr'.base}{T}
\rulerCmdUse{rules.T.expr'.base.e.cast}
\hspace{1ex}
\rulerCmdUse{rules.T.expr'.base.e.app.coe}
\end{rulerRulesetFigure}
}

\rulerCmdDef{rules.F.kind.base.scheme}{%
\ensuremath{| env :- | _{ | k | } |  t | }
}
\rulerCmdDef{rules.F.kind.base.t.con}{%
\rulerRule{t.con}{F}
{%
| identc `elem` env | 
}
{%
| env :- | _{ | k | } |  identc | 
}
}

\rulerCmdDef{rules.F.kind.base.t.var}{%
\rulerRule{t.var}{F}
{%
| identx `elem` env | 
}
{%
| env :- | _{ | k | } |  identx | 
}
}

\rulerCmdDef{rules.F.kind.base.t.app}{%
\rulerRule{t.app}{F}
{%
| env :- | _{ | k | } |  a | 
\\
| env :- | _{ | k | } |  f | 
}
{%
| env :- | _{ | k | } |  f a | 
}
}

\rulerCmdDef{rules.F.kind.base.t.forall}{%
\rulerRule{t.forall}{F}
{%
| alpha , env :- | _{ | k | } |  ty | 
}
{%
| env :- | _{ | k | } |  forall ^ alpha ^ dot ty | 
}
}

\rulerCmdDef{rules.FE.kind.base.scheme}{%
\ensuremath{| env :- | _{ | k | } |  t | }
}
\rulerCmdDef{rules.FE.kind.base.t.con}{%
\rulerRule{t.con}{FE}
{%
| identc `elem` env | 
}
{%
| env :- | _{ | k | } |  identc | 
}
}

\rulerCmdDef{rules.FE.kind.base.t.var}{%
\rulerRule{t.var}{FE}
{%
| identx `elem` env | 
}
{%
| env :- | _{ | k | } |  identx | 
}
}

\rulerCmdDef{rules.FE.kind.base.t.app}{%
\rulerRule{t.app}{FE}
{%
| env :- | _{ | k | } |  a | 
\\
| env :- | _{ | k | } |  f | 
}
{%
| env :- | _{ | k | } |  f a | 
}
}

\rulerCmdDef{rules.FE.kind.base.t.forall}{%
\rulerRule{t.forall}{FE}
{%
| alpha , env :- | _{ | k | } |  ty | 
}
{%
| env :- | _{ | k | } |  forall ^ alpha ^ dot ty | 
}
}

\rulerCmdDef{rules.FE.kind.base.t.exists}{%
\rulerRule{t.exists}{FE}
{%
| alpha , env :- | _{ | k | } |  ty | 
}
{%
| env :- | _{ | k | } |  exists alpha dot ty | 
}
}

\rulerCmdDef{rules.G.kind.base.scheme}{%
\ensuremath{| env :- | _{ | k | } |  t | }
}
\rulerCmdDef{rules.G.kind.base.t.con}{%
\rulerRule{t.con}{G}
{%
| identc `elem` env | 
}
{%
| env :- | _{ | k | } |  identc | 
}
}

\rulerCmdDef{rules.G.kind.base.t.var}{%
\rulerRule{t.var}{G}
{%
| identx `elem` env | 
}
{%
| env :- | _{ | k | } |  identx | 
}
}

\rulerCmdDef{rules.G.kind.base.t.app}{%
\rulerRule{t.app}{G}
{%
| env :- | _{ | k | } |  a | 
\\
| env :- | _{ | k | } |  f | 
}
{%
| env :- | _{ | k | } |  f a | 
}
}

\rulerCmdDef{rules.G.kind.base.t.forall}{%
\rulerRule{t.forall}{G}
{%
| alpha , env :- | _{ | k | } |  ty | 
}
{%
| env :- | _{ | k | } |  forall ^ alpha ^ dot ty | 
}
}

\rulerCmdDef{rules.G.kind.base.t.exists}{%
\rulerRule{t.exists}{G}
{%
| alpha , env :- | _{ | k | } |  ty | 
}
{%
| env :- | _{ | k | } |  exists alpha dot ty | 
}
}

\rulerCmdDef{rules.G.kind.base.t.eqs}{%
\rulerRule{t.eqs}{G}
{%
| env :- | _{ | k | } |  ty | 
\\
| env :- | _{ | k | } |  ty | _{ | i | }^{ | l | } |  | 
\\
| env :- | _{ | k | } |  ty | _{ | i | }^{ | r | } |  | 
\\
| ty | _{ | i | }^{ | l | } |  =*= ty | _{ | i | }^{ | r | } |  `elem` env | 
}
{%
| env :- | _{ | k | } |  ( | \overline{ | ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty | 
}
}

\rulerCmdDef{rules.T.kind.base.scheme}{%
\ensuremath{| env :- | _{ | k | } |  t | }
}
\rulerCmdDef{rules.T.kind.base.t.con}{%
\rulerRule{t.con}{T}
{%
| identc `elem` env | 
}
{%
| env :- | _{ | k | } |  identc | 
}
}

\rulerCmdDef{rules.T.kind.base.t.var}{%
\rulerRule{t.var}{T}
{%
| identx `elem` env | 
}
{%
| env :- | _{ | k | } |  identx | 
}
}

\rulerCmdDef{rules.T.kind.base.t.app}{%
\rulerRule{t.app}{T}
{%
| env :- | _{ | k | } |  a | 
\\
| env :- | _{ | k | } |  f | 
}
{%
| env :- | _{ | k | } |  f a | 
}
}

\rulerCmdDef{rules.T.kind.base.t.forall}{%
\rulerRule{t.forall}{T}
{%
| alpha , env :- | _{ | k | } |  ty | 
}
{%
| env :- | _{ | k | } |  forall ^ alpha ^ dot ty | 
}
}

\rulerCmdDef{rules.T.kind.base.t.exists}{%
\rulerRule{t.exists}{T}
{%
| alpha , env :- | _{ | k | } |  ty | 
}
{%
| env :- | _{ | k | } |  exists alpha dot ty | 
}
}

\rulerCmdDef{rules.T.kind.base.t.eqs}{%
\rulerRule{t.eqs}{T}
{%
| env :- | _{ | k | } |  ty | 
\\
| env :- | _{ | k | } |  ty | _{ | i | }^{ | l | } |  | 
\\
| env :- | _{ | k | } |  ty | _{ | i | }^{ | r | } |  | 
\\
| ty | _{ | i | }^{ | l | } |  =*= ty | _{ | i | }^{ | r | } |  `elem` env | 
}
{%
| env :- | _{ | k | } |  ( | \overline{ | ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty | 
}
}

\rulerCmdDef{rules.F.kind.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.F.kind.base.scheme}}{Well-formedness rules}{rules.F.kind.base}{F}
\rulerCmdUse{rules.F.kind.base.t.con}
\hspace{1ex}
\rulerCmdUse{rules.F.kind.base.t.var}
\hspace{1ex}
\rulerCmdUse{rules.F.kind.base.t.app}
\hspace{1ex}
\rulerCmdUse{rules.F.kind.base.t.forall}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.FE.kind.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.FE.kind.base.scheme}}{Well-formedness rules}{rules.FE.kind.base}{FE}
\rulerCmdUse{rules.FE.kind.base.t.con}
\hspace{1ex}
\rulerCmdUse{rules.FE.kind.base.t.var}
\hspace{1ex}
\rulerCmdUse{rules.FE.kind.base.t.app}
\hspace{1ex}
\rulerCmdUse{rules.FE.kind.base.t.forall}
\hspace{1ex}
\rulerCmdUse{rules.FE.kind.base.t.exists}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.G.kind.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.G.kind.base.scheme}}{Well-formedness rules}{rules.G.kind.base}{G}
\rulerCmdUse{rules.G.kind.base.t.con}
\hspace{1ex}
\rulerCmdUse{rules.G.kind.base.t.var}
\hspace{1ex}
\rulerCmdUse{rules.G.kind.base.t.app}
\hspace{1ex}
\rulerCmdUse{rules.G.kind.base.t.forall}
\hspace{1ex}
\rulerCmdUse{rules.G.kind.base.t.exists}
\hspace{1ex}
\rulerCmdUse{rules.G.kind.base.t.eqs}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.T.kind.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.T.kind.base.scheme}}{Well-formedness rules}{rules.T.kind.base}{T}
\rulerCmdUse{rules.T.kind.base.t.con}
\hspace{1ex}
\rulerCmdUse{rules.T.kind.base.t.var}
\hspace{1ex}
\rulerCmdUse{rules.T.kind.base.t.app}
\hspace{1ex}
\rulerCmdUse{rules.T.kind.base.t.forall}
\hspace{1ex}
\rulerCmdUse{rules.T.kind.base.t.exists}
\hspace{1ex}
\rulerCmdUse{rules.T.kind.base.t.eqs}
\end{rulerRulesetFigure}
}

\rulerCmdDef{rules.F.pat.base.scheme}{%
\ensuremath{| env ; envl :- | _{ | p | } |  p : ty | }
}
\rulerCmdDef{rules.F.pat.base.p.con}{%
\rulerRule{p.con}{F}
{%
| env (identc | ^{ | unp | } | ) = ty | 
}
{%
| env ; emptyenvl :- | _{ | p | } |  identc : ty | 
}
}

\rulerCmdDef{rules.F.pat.base.p.var}{%
\rulerRule{p.var}{F}
{%
| envl (identx) = ty | 
}
{%
| env ; envl :- | _{ | p | } |  identx :: ty : ty | 
}
}

\rulerCmdDef{rules.F.pat.base.p.app.pat}{%
\rulerRule{p.app.pat}{F}
{%
| env ; envl :- | _{ | p | } |  a : ty | ^{ | a | } |  | 
\\
| env ; envl :- | _{ | p | } |  f : ty | ^{ | a | } |  -> ty | 
}
{%
| env ; envl :- | _{ | p | } |  f a : ty | 
}
}

\rulerCmdDef{rules.F.pat.base.p.app.univ}{%
\rulerRule{p.app.univ}{F}
{%
| env ; envl :- | _{ | p | } |  f : forall ^ alpha ^ dot ty | 
}
{%
| env ; envl :- | _{ | p | } |  f ty | ^{ | a | } |  : (subst tya alpha) ty | 
}
}

\rulerCmdDef{rules.FE.pat.base.scheme}{%
\ensuremath{| env ; envl :- | _{ | p | } |  p : ty | }
}
\rulerCmdDef{rules.FE.pat.base.p.con}{%
\rulerRule{p.con}{FE}
{%
| env (identc | ^{ | unp | } | ) = ty | 
}
{%
| env ; emptyenvl :- | _{ | p | } |  identc : ty | 
}
}

\rulerCmdDef{rules.FE.pat.base.p.var}{%
\rulerRule{p.var}{FE}
{%
| envl (identx) = ty | 
}
{%
| env ; envl :- | _{ | p | } |  identx :: ty : ty | 
}
}

\rulerCmdDef{rules.FE.pat.base.p.app.pat}{%
\rulerRule{p.app.pat}{FE}
{%
| env ; envl :- | _{ | p | } |  a : ty | ^{ | a | } |  | 
\\
| env ; envl :- | _{ | p | } |  f : ty | ^{ | a | } |  -> ty | 
}
{%
| env ; envl :- | _{ | p | } |  f a : ty | 
}
}

\rulerCmdDef{rules.FE.pat.base.p.app.univ}{%
\rulerRule{p.app.univ}{FE}
{%
| env ; envl :- | _{ | p | } |  f : forall ^ alpha ^ dot ty | 
}
{%
| env ; envl :- | _{ | p | } |  f ty | ^{ | a | } |  : (subst tya alpha) ty | 
}
}

\rulerCmdDef{rules.FE.pat.base.p.app.exist}{%
\rulerRule{p.app.exist}{FE}
{%
| env ; envl :- | _{ | p | } |  f : exists alpha dot ty | 
\\
| identv `elem` envl |  \hspace{2ex} | identv notelem ftv (env) | 
}
{%
| env ; envl :- | _{ | p | } |  f identv : (subst identv alpha) ty | 
}
}

\rulerCmdDef{rules.G.pat.base.scheme}{%
\ensuremath{| env ; envl :- | _{ | p | } |  p : ty | }
}
\rulerCmdDef{rules.G.pat.base.p.con}{%
\rulerRule{p.con}{G}
{%
| env (identc | ^{ | unp | } | ) = ty | 
}
{%
| env ; emptyenvl :- | _{ | p | } |  identc : ty | 
}
}

\rulerCmdDef{rules.G.pat.base.p.var}{%
\rulerRule{p.var}{G}
{%
| envl (identx) = ty | 
}
{%
| env ; envl :- | _{ | p | } |  identx :: ty : ty | 
}
}

\rulerCmdDef{rules.G.pat.base.p.app.pat}{%
\rulerRule{p.app.pat}{G}
{%
| env ; envl :- | _{ | p | } |  a : ty | ^{ | a | } |  | 
\\
| env ; envl :- | _{ | p | } |  f : ty | ^{ | a | } |  -> ty | 
}
{%
| env ; envl :- | _{ | p | } |  f a : ty | 
}
}

\rulerCmdDef{rules.G.pat.base.p.app.univ}{%
\rulerRule{p.app.univ}{G}
{%
| env ; envl :- | _{ | p | } |  f : forall ^ alpha ^ dot ty | 
}
{%
| env ; envl :- | _{ | p | } |  f ty | ^{ | a | } |  : (subst tya alpha) ty | 
}
}

\rulerCmdDef{rules.G.pat.base.p.app.exist}{%
\rulerRule{p.app.exist}{G}
{%
| env ; envl :- | _{ | p | } |  f : exists alpha dot ty | 
\\
| identv `elem` envl |  \hspace{2ex} | identv notelem ftv (env) | 
}
{%
| env ; envl :- | _{ | p | } |  f identv : (subst identv alpha) ty | 
}
}

\rulerCmdDef{rules.G.pat.base.p.app.eqs}{%
\rulerRule{p.app.eqs}{G}
{%
| env ; envl :- | _{ | p | } |  f : ( | \overline{ | ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty |  \hspace{2ex} | ty | _{ | i | }^{ | l | } |  =*= ty | _{ | i | }^{ | r | } |  `elem` envl | 
}
{%
| env ; envl :- | _{ | p | } |  f : ty | 
}
}

\rulerCmdDef{rules.T.pat.base.scheme}{%
\ensuremath{| env ; envl :- | _{ | p | } |  p : ty ~> p' | }
}
\rulerCmdDef{rules.T.pat.base.p.con}{%
\rulerRule{p.con}{T}
{%
| env (identc | ^{ | unp | } | ) = ty | 
}
{%
| env ; emptyenvl :- | _{ | p | } |  identc : ty ~> identc | 
}
}

\rulerCmdDef{rules.T.pat.base.p.var}{%
\rulerRule{p.var}{T}
{%
| envl (identx) = ty | 
}
{%
| env ; envl :- | _{ | p | } |  identx :: ty : ty ~> identx :: ty | 
}
}

\rulerCmdDef{rules.T.pat.base.p.app.pat}{%
\rulerRule{p.app.pat}{T}
{%
| env ; envl :- | _{ | p | } |  a : ty | ^{ | a | } |  ~> a' | 
\\
| env ; envl :- | _{ | p | } |  f : ty | ^{ | a | } |  -> ty ~> f' | 
}
{%
| env ; envl :- | _{ | p | } |  f a : ty ~> f' a' | 
}
}

\rulerCmdDef{rules.T.pat.base.p.app.univ}{%
\rulerRule{p.app.univ}{T}
{%
| env ; envl :- | _{ | p | } |  f : forall ^ alpha ^ dot ty ~> f' | 
}
{%
| env ; envl :- | _{ | p | } |  f ty | ^{ | a | } |  : (subst tya alpha) ty ~> f' ty | ^{ | a | } |  | 
}
}

\rulerCmdDef{rules.T.pat.base.p.app.exist}{%
\rulerRule{p.app.exist}{T}
{%
| env ; envl :- | _{ | p | } |  f : exists alpha dot ty ~> f' | 
\\
| identv `elem` envl |  \hspace{2ex} | identv notelem ftv (env) | 
}
{%
| env ; envl :- | _{ | p | } |  f identv : (subst identv alpha) ty ~> f' identv | 
}
}

\rulerCmdDef{rules.T.pat.base.p.app.eqs}{%
\rulerRule{p.app.eqs}{T}
{%
| env ; envl :- | _{ | p | } |  f : ( | \overline{ | ty | ^{ | l | } |  =*= ty | ^{ | r | } |  | } | ) => ty ~> p' |  \hspace{2ex} | envl (identv | _{ | i | } | ) = (ty | _{ | i | }^{ | l | } |  =*= ty | _{ | i | }^{ | r | } | ) | 
}
{%
| env ; envl :- | _{ | p | } |  f : ty ~> f'  | \overline{ | identv | } |  | 
}
}

\rulerCmdDef{rules.F.pat.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.F.pat.base.scheme}}{Pattern type rules}{rules.F.pat.base}{F}
\rulerCmdUse{rules.F.pat.base.p.con}
\hspace{1ex}
\rulerCmdUse{rules.F.pat.base.p.var}
\hspace{1ex}
\rulerCmdUse{rules.F.pat.base.p.app.pat}
\hspace{1ex}
\rulerCmdUse{rules.F.pat.base.p.app.univ}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.FE.pat.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.FE.pat.base.scheme}}{Pattern type rules}{rules.FE.pat.base}{FE}
\rulerCmdUse{rules.FE.pat.base.p.con}
\hspace{1ex}
\rulerCmdUse{rules.FE.pat.base.p.var}
\hspace{1ex}
\rulerCmdUse{rules.FE.pat.base.p.app.pat}
\hspace{1ex}
\rulerCmdUse{rules.FE.pat.base.p.app.univ}
\hspace{1ex}
\rulerCmdUse{rules.FE.pat.base.p.app.exist}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.G.pat.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.G.pat.base.scheme}}{Pattern type rules}{rules.G.pat.base}{G}
\rulerCmdUse{rules.G.pat.base.p.con}
\hspace{1ex}
\rulerCmdUse{rules.G.pat.base.p.var}
\hspace{1ex}
\rulerCmdUse{rules.G.pat.base.p.app.pat}
\hspace{1ex}
\rulerCmdUse{rules.G.pat.base.p.app.univ}
\hspace{1ex}
\rulerCmdUse{rules.G.pat.base.p.app.exist}
\hspace{1ex}
\rulerCmdUse{rules.G.pat.base.p.app.eqs}
\end{rulerRulesetFigure}
}
\rulerCmdDef{rules.T.pat.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.T.pat.base.scheme}}{Pattern type rules}{rules.T.pat.base}{T}
\rulerCmdUse{rules.T.pat.base.p.con}
\hspace{1ex}
\rulerCmdUse{rules.T.pat.base.p.var}
\hspace{1ex}
\rulerCmdUse{rules.T.pat.base.p.app.pat}
\hspace{1ex}
\rulerCmdUse{rules.T.pat.base.p.app.univ}
\hspace{1ex}
\rulerCmdUse{rules.T.pat.base.p.app.exist}
\hspace{1ex}
\rulerCmdUse{rules.T.pat.base.p.app.eqs}
\end{rulerRulesetFigure}
}

\rulerCmdDef{rules.T.spine.base.scheme}{%
\ensuremath{| coeIn ;  | \overline{ | coeIn | } |  ; env :- | _{ | s | } |  ty | ^{ | a | } |  ~~ ty | ^{ | b | } |  ~> coe ;  | \overline{ | coeOut | } |  | }
}
\rulerCmdDef{rules.T.spine.base.s.app}{%
\rulerRule{s.app}{T}
{%
| coeIn | ^{ | i | } |  ;  | \overline{ | coeIn | ^{ | ir | }} |  ; env :- | _{ | s | } |  ty | ^{ | b | } |  ~~ ty | ^{ | a | } |  ~> coe | ^{ | r | } |  ;  | \overline{ | coeOut | ^{ | r | }} |  | 
\\
| coeIn | ^{ | i | } |  ;  | \overline{ | coeIn | ^{ | il | }} |  ; env :- | _{ | s | } |  ty | ^{ | f | } |  ~~ ty | ^{ | g | } |  ~> coe | ^{ | l | } |  ;  | \overline{ | coeOut | ^{ | l | }} |  | 
}
{%
| coeIn | ^{ | i | } |  ;  | \overline{ | coeIn | ^{ | il | }} |   | \overline{ | coeIn | ^{ | ir | }} |  ; env :- | _{ | s | } |  ty | ^{ | f | } |  ty | ^{ | a | } |  ~~ ty | ^{ | g | } |  ty | ^{ | b | } |  ~> coe | ^{ | l | } |  coe | ^{ | r | } |  ;  | \overline{ | left coeOut | ^{ | l | } |  | } |  ^^^  | \overline{ | right coeOut | ^{ | r | } |  | } |  | 
}
}

\rulerCmdDef{rules.T.spine.base.s.univ}{%
\rulerRule{s.univ}{T}
{%
| coeIn | ^{ | i | } |  ;  | \overline{ | coeIn | ^{ | i | }} |  ; env :- | _{ | s | } |  ty | ^{ | a | } |  ~~ ty | ^{ | b | } |  ~>  | \overline{ | coe | } |  ; coe | 
\\
| v notelem ftv (env) | 
}
{%
| coeIn | ^{ | i | } |  ;  | \overline{ | coeIn | ^{ | i | }} |  ; env :- | _{ | s | } |  forall ^ alpha ^ dot ty | ^{ | a | } |  ~~ forall ^ alpha ^ dot ty | ^{ | b | } |  ~>  | \overline{ | coe @ alpha | } |  ; forall ^ alpha ^ dot coe | 
}
}

\rulerCmdDef{rules.T.spine.base.s.refl}{%
\rulerRule{s.refl}{T}
{%
}
{%
| _ ^^^  ; emptyset ; env :- | _{ | s | } |  ty ~~ ty ~> emptyset ; ty | 
}
}

\rulerCmdDef{rules.T.spine.base.s.uneq}{%
\rulerRule{s.uneq}{T}
{%
}
{%
| coeIn | ^{ | i | } |  ; coe ; env :- | _{ | s | } |  ty | ^{ | a | } |  ~~ ty | ^{ | b | } |  ~> coeIn | ^{ | i | } |  ; coe | 
}
}

\rulerCmdDef{rules.T.spine.base}{%
\begin{rulerRulesetFigure}{\rulerCmdUse{rules.T.spine.base.scheme}}{Coercion construction and deconstruction by spine}{rules.T.spine.base}{T}
\rulerCmdUse{rules.T.spine.base.s.app}
\hspace{1ex}
\rulerCmdUse{rules.T.spine.base.s.univ}
\hspace{1ex}
\rulerCmdUse{rules.T.spine.base.s.refl}
\hspace{1ex}
\rulerCmdUse{rules.T.spine.base.s.uneq}
\end{rulerRulesetFigure}
}