%%\Head{Syntax}
%%\Subhead{Constants}
c : type.                               %name c C.

%%\Subhead{Principals}
p : type.                               %name p P.
pc : c -> p.
pcat : p -> p -> p.

%%\Subhead{Labels}
l : type.                               %name l L.
lp : p -> p -> l.
lcat : l -> l -> l.

%%\Subhead{Hierarchies}
a : type.                               %name a A.
az : a.
ap : a -> p -> p -> a.

%%\Subhead{Types}
t : type.                               %name t T.
tbool : l -> t.
tfun : t -> t -> t.

%%\Subhead{Variables}
x : type.                               %name x X.

%%\Subhead{Terms}
e : type.                               %name e E.
true : l -> e.
false : l -> e.
var : x -> e.
fun : a -> x -> t -> e -> e.
app : e -> e -> e.
ifb : e -> e -> e -> e.
ifp : p -> p -> e -> e -> e.
tag : l -> l -> e -> e.

%%\Subhead{Contexts}
g : type.                               %name g G.
gz : g.
gx : g -> x -> t -> g.


%%\Head{Static semantics}
%%\Subhead{Substitutions}
sub : e -> e -> x -> e -> type.       %name sub Sub.
%mode sub +E1 +E2 +X -E3.
sub-true : sub (true L) E X (true L).
sub-false : sub (false L) E X (false L).
sub-var1 : sub (var X) E X E.
sub-var2 : sub (var X1) E X2 (var X1).
sub-fun : sub (fun A X1 T E1) E X (fun A X1 T E2)
  <- sub E1 E X E2.
sub-app : sub (app E1 E2) E X (app E3 E4)
  <- sub E1 E X E3
  <- sub E2 E X E4.
sub-ifb : sub (ifb E1 E2 E3) E X (ifb E4 E5 E6)
  <- sub E1 E X E4
  <- sub E2 E X E5
  <- sub E3 E X E6.
sub-ifp : sub (ifp P1 P2 E1 E2) E X (ifp P1 P2 E3 E4) 
  <- sub E1 E X E3
  <- sub E2 E X E4.
sub-tag : sub (tag L1 L2 E1) E X (tag L1 L2 E2)
  <- sub E1 E X E2.

%%\Subhead{Principal subtypings}
psome : p -> type.
%mode psome -P.

pst : a -> p -> p -> type.
pnst : a -> p -> p -> type.
%mode pst +A +P1 +P2.
%mode pnst +A +P1 +P2.

pst-z : pst A P P.
pst-x : pst A P1 P3
  <- psome P2
  <- pst A P1 P2
  <- pst A P2 P3.
pst-a1 : pst (ap A P1 P2) P1 P2.
pst-a2 : pst (ap A P1 P2) P3 P4
  <- pst A P3 P4.
pst-cat1 : pst A (pcat P1 P2) P1.
pst-cat2 : pst A (pcat P1 P2) P2.

%%\Subhead{Label subtypings}
lst : a -> l -> l -> type.
lnst : a -> l -> l -> type.
%mode lst +A +L1 +L2.
%mode lnst +A +L1 +L2.

lsome : l -> type.
%mode lsome -L.

lst-z : lst A L L.
lst-x : lst A L1 L3
  <- lsome L2
  <- lst A L1 L2
  <- lst A L2 L3.
lst-p : lst A (lp P1 P2) (lp P3 P4)
  <- pst A P1 P3
  <- pst A P2 P4.
lst-cat1 : lst A L1 (lcat L1 L2).
lst-cat2 : lst A L2 (lcat L1 L2).

%%\Subhead{Hierarchy subtypings}
asome : a -> type.
%mode asome -A.

ast : a -> a -> type.
%mode ast +A1 +A2.
ast-z : ast A A.
ast-x : ast A1 A3
  <- asome A2
  <- ast A1 A2
  <- ast A2 A3.
ast-p1 : ast (ap A1 P1 P2) A2
  <- ast A1 A2.
ast-p2 : ast A1 (ap A2 P3 P4)
  <- ast A1 A2
  <- pst A1 P3 P4.

%%\Subhead{Type subtypings}
tst : a -> t -> t -> type.
%mode tst +A +T1 +T2.
tst-bool : tst A (tbool L1) (tbool L2)
  <- lst A L1 L2.
tst-fun : tst A (tfun T1 T2) (tfun T3 T4)
  <- tst A T3 T1
  <- tst A T2 T4.

%%\Subhead{Type labels}
lab : t -> l -> type.
%mode lab +T -L.
lab-bool : lab (tbool L) L.
lab-fun : lab (tfun T1 T2) L
  <- lab T2 L.

%%\Subhead{Typings}
ty : a -> g -> e -> t -> type.
%mode ty +A +G +E -T.
ty-true : ty A G (true L) (tbool L).
ty-false : ty A G (false L) (tbool L).
ty-ifb : ty A G (ifb E1 E2 E3) T
  <- ty A G E1 (tbool L)
  <- ty A G E2 T
  <- ty A G E3 T
  <- lab T L.
ty-var1 : ty A (gx G X T) (var X) T.
ty-var2 : ty A (gx G X1 T1) (var X2) T2
  <- ty A G (var X2) T2.
ty-fun : ty A G (fun A1 X T1 E) (tfun T1 T2)
  <- ast A A1
  <- ty A1 (gx G X T1) E T2.
ty-app : ty A G (app E1 E2) T2
  <- ty A G E1 (tfun T1 T2)
  <- ty A G E2 T1.
ty-ifp : ty A G (ifp P1 P2 E1 E2) T
  <- ty (ap A P1 P2) G E1 T
  <- ty A G E2 T.
ty-tag : ty A G (tag L1 L2 E) (tbool L2)
  <- lst A L1 L2
  <- ty A G E (tbool L1).

%%\Head{Dynamic semantics}
%%\Subhead{Values}
val : e -> type.                        %name val Val.
%mode val +E.
val-true : val (true L).
val-false : val (false L).
val-fun : val (fun A X T E).

%%\Subhead{Holes}
q : type.                               %name q Q.
qappa : e -> q.
qappb : e -> q.
qifb : e -> e -> q.
qtag : l -> l -> q.

%%\Subhead{Splits}
split : e -> q -> e -> type.            %name split Split.
%mode split +E1 -Q -E2.
split-ifb : split (ifb E1 E2 E3) (qifb E2 E3) E1.
split-app1 : split (app E1 E2) (qappa E2) E1.
split-app2 : split (app E1 E2) (qappb E1) E2.
split-tag : split (tag L1 L2 E) (qtag L1 L2) E.

%%\Subhead{Combines}
combine : q -> e -> e -> type.               %name combine Combine.
%mode combine +Q +E1 -E2.
combine-app1 : combine (qappa E2) E1 (app E1 E2).
combine-app2 : combine (qappb E1) E2 (app E1 E2).
combine-ifb : combine (qifb E2 E3) E1 (ifb E1 E2 E3).
combine-tag : combine (qtag L1 L2) E (tag L1 L2 E).

%%\Subhead{Small-step evaluations}
ev : a -> e -> e -> type.
%mode ev +A +E1 -E2.
ev-app : ev A (app (fun A1 X T E1) E2) E3 
  <- val E2
  <- sub E1 E2 X E3.
ev-ifb1 : ev A (ifb (true L) E1 E2) E1.
ev-ifb2 : ev A (ifb (false L) E1 E2) E2.
ev-ifp1 : ev A (ifp P1 P2 E1 E2) E1
  <- pst A P1 P2.
ev-ifp2 : ev A (ifp P1 P2 E1 E2) E2
  <- pnst A P1 P2.
ev-tag1 : ev A (tag L1 L2 (true L1)) (true L2).
ev-tag2 : ev A (tag L1 L2 (false L1)) (false L2).
ev-hole : ev A E1 E4 
  <- split E1 Q E2
  <- ev A E2 E3
  <- combine Q E3 E4.

%%\Subhead{Tag checkings}
ae : a -> e -> type.
%mode ae +A +E.
ae-true : ae A (true L).
ae-false : ae A (false L).
ae-fun : ae A (fun A1 X T E)
  <- ast A A1.
ae-app : ae A (app E1 E2)
  <- ae A E1
  <- ae A E2.
ae-ifb : ae A (ifb E1 E2 E3)
  <- ae A E1
  <- ae A E2
  <- ae A E3.
ae-ifp : ae A (ifp P1 P2 E1 E2)
  <- ae (ap A P1 P2) E1
  <- ae A E2.
ae-tag : ae A (tag L1 L2 E)
  <- lst A L1 L2
  <- ae A E.

%%\Subhead{Top-level evaluations}
topev : a -> e -> a -> a -> e -> type.
%mode topev +A1 +E1 +A -A2 -E2.
topev-ev : topev A E1 A A E2
  <- ev A E1 E2.
topev-upd : topev A1 E A2 A2 E
  <- ae A2 E.

%%\Subhead{Totalities}
asome-total : asome A -> type.
%mode +{A:a} -{Asome:asome A} (asome-total Asome).

sub-total : sub E1 E X E2 -> type.
%mode sub-total -Sub.

psty : a -> p -> p -> type.
%mode psty +A +P1 +P2.
psty-pst : psty A P1 P2
  <- pst A P1 P2.
psty-pnst : psty A P1 P2
  <- pnst A P1 P2.

pst-total : psty A P1 P2 -> type.
%mode pst-total -Psty.

%%\Subhead{Program evaluations}
bigev : a -> e -> a -> e -> type.
%mode bigev +A1 +E1 -A2 -E2.
bigev-v : bigev A E A E
  <- val E.
bigev-e : bigev A1 E1 A2 E3
  <- asome A
  <- topev A1 E1 A A2 E2
  <- bigev A2 E2 A3 E3.

%%\Head{Lemmas}
%%\Subhead{Principal subtypings} 
appst : pst A P1 P2 -> pst (ap A P3 P4) P1 P2 -> type. 
%mode appst +Pst1 -Pst2.
%mode +{A} +{P1} +{P2} +{P3} +{P4} +{Pst1:pst A P1 P2}
   -{Pst2:pst (ap A P3 P4) P1 P2} (appst Pst1 Pst2).
appst-z : appst pst-z pst-z.
appst-x : appst (pst-x Pst2 Pst1 Some) (pst-x Pst4 Pst3 Some)
  <- appst Pst1 Pst3
  <- appst Pst2 Pst4.
appst-a1 : appst pst-a1 (pst-a2 pst-a1).
appst-a2 : appst (pst-a2 Pst1) (pst-a2 Pst3)
  <- appst Pst1 Pst3.
appst-cat1 : appst pst-cat1 pst-cat1.
appst-cat2 : appst pst-cat2 pst-cat2.

pstpst : pst (ap A P1 P2) P3 P4 -> pst A P1 P2 -> pst A P3 P4 -> type.
%mode pstpst +Pst1 +Pst2 -Pst3.
pstpst-z : pstpst pst-z Pst pst-z.
pstpst-x : pstpst (pst-x Pst2 Pst1 Some) Pst3 (pst-x Pst5 Pst4 Some)
  <- pstpst Pst1 Pst3 Pst4
  <- pstpst Pst2 Pst3 Pst5.
pstpst-a1 : pstpst pst-a1 Pst Pst.
pstpst-a2 : pstpst (pst-a2 Pst1) Pst2 Pst1.
pstpst-cat1 : pstpst pst-cat1 Pst pst-cat1.
pstpst-cat2 : pstpst pst-cat2 Pst pst-cat2.

astpst : pst A1 P1 P2 -> ast A2 A1 -> pst A2 P1 P2 -> type. 
%mode astpst +Pst1 +Ast -Pst2.
astpst-z : astpst pst-z Ast pst-z.
astpst-x : astpst (pst-x Pst2 Pst1 Psome) Ast (pst-x Pst4 Pst3 Psome)
  <- astpst Pst1 Ast Pst3
  <- astpst Pst2 Ast Pst4.
astpst-a1 : astpst pst-a1 Ast pst-a1.
astpst-a2 : astpst (pst-a2 Pst1) (ast-p2 Pst3 Ast1) Pst2
  <- astpst Pst1 Ast1 Pst2.
astpst-cat1 : astpst pst-cat1 Ast pst-cat1.
astpst-cat2 : astpst pst-cat2 Ast pst-cat2.

%%\Subhead{Label subtypings} 
pstlst : lst (ap A P1 P2) L1 L2 -> pst A P1 P2 -> lst A L1 L2 -> type.
%mode pstlst +Lst1 +Pst2 -Lst2.
pstlst-z : pstlst lst-z Pst lst-z.
pstlst-x : pstlst (lst-x Lst2 Lst1 Psome) Pst (lst-x Lst4 Lst3 Psome)
  <- pstlst Lst1 Pst Lst3
  <- pstlst Lst2 Pst Lst4.
pstlst-p : pstlst (lst-p Pst2 Pst1) Pst (lst-p Pst4 Pst3)
  <- pstpst Pst1 Pst Pst3
  <- pstpst Pst2 Pst Pst4.
pstlst-cat1 : pstlst lst-cat1 Pst lst-cat1.
pstlst-cat2 : pstlst lst-cat2 Pst lst-cat2.

astlst : lst A1 L1 L2 -> ast A2 A1 -> lst A2 L1 L2 -> type. 
%mode astlst +Lst1 +Ast -Lst2.
astlst-z : astlst lst-z Ast lst-z.
astlst-x : astlst (lst-x Lst2 Lst1 Lsome) Ast (lst-x Lst4 Lst3 Lsome)
  <- astlst Lst1 Ast Lst3
  <- astlst Lst2 Ast Lst4.
astlst-p : astlst (lst-p Pst2 Pst1) Ast (lst-p Pst4 Pst3)
  <- astpst Pst1 Ast Pst3
  <- astpst Pst2 Ast Pst4.
astlst-cat1 : astlst lst-cat1 Pst lst-cat1.
astlst-cat2 : astlst lst-cat2 Pst lst-cat2.

%%\Subhead{Hierarchy subtypings}
pstast : ast (ap A1 P1 P2) A2 -> pst A1 P1 P2 -> ast A1 A2 -> type.
%mode pstast +Ast1 +Pst -Ast2.
% no pstast-z because A1 = A2 != ap A1 P1 P2
pstast-x : pstast (ast-x Ast2 Ast1 Asome) Pst (ast-x Ast2 Ast3 Asome)
  <- pstast Ast1 Pst Ast3.
pstast-p1 : pstast (ast-p1 Ast) Pst Ast.
pstast-p2 : pstast (ast-p2 Pst1 Ast1) Pst2 (ast-p2 Pst3 Ast2)
  <- pstast Ast1 Pst2 Ast2
  <- pstpst Pst1 Pst2 Pst3.

apast : ast A1 A2 -> ast (ap A1 P1 P2) A2 -> type.
%mode +{A1} +{A2} +{P1} +{P2} +{Ast1:ast A1 A2} 
  -{Ast2:ast (ap A1 P1 P2) A2} (apast Ast1 Ast2).
apast-z : apast ast-z (ast-p1 ast-z).
apast-x : apast (ast-x Ast2 Ast1 Asome) (ast-x Ast2 Ast3 Asome)
  <- apast Ast1 Ast3.
apast-p1 : apast (ast-p1 Ast1) (ast-p1 Ast2)
  <- apast Ast1 Ast2.
apast-p2 : apast (ast-p2 Lst1 Ast1) (ast-p2 Lst2 Ast2)
  <- apast Ast1 Ast2
  <- appst Lst1 Lst2.

apapast : ast A1 A2 -> ast (ap A1 P1 P2) (ap A2 L1 L2) -> type.
%mode +{A1} +{A2} +{P1} +{P2} +{Ast1:ast A1 A2} 
  -{Ast2:ast (ap A1 P1 P2) (ap A2 P1 P2)} (apapast Ast1 Ast2).
apapast-l : apapast Ast (ast-p2 pst-a1 Ast2)
  <- apast Ast Ast2.

%%\Subhead{Type subtypings}
pstty : ty (ap A P1 P2) G E T -> pst A P1 P2 -> ty A G E T -> type.
%mode pstty +Ty1 +Pst -Ty2.
pstty-true : pstty ty-true Pst ty-true.
pstty-false : pstty ty-false Pst ty-false.
pstty-ifb : pstty (ty-ifb Pab Ty3 Ty2 Ty1) Pst (ty-ifb Pab Ty4 Ty5 Ty6)
  <- pstty Ty1 Pst Ty4
  <- pstty Ty2 Pst Ty5
  <- pstty Ty3 Pst Ty6.
pstty-var1 : pstty ty-var1 Pst ty-var1.
pstty-var2 : pstty (ty-var2 Ty1) Pst (ty-var2 Ty2)
  <- pstty Ty1 Pst Ty2.
pstty-fun : pstty (ty-fun Ty Ast1) Pst (ty-fun Ty Ast2)
  <- pstast Ast1 Pst Ast2.
pstty-app : pstty (ty-app Ty2 Ty1) Pst (ty-app Ty4 Ty3)
  <- pstty Ty1 Pst Ty3
  <- pstty Ty2 Pst Ty4.
pstty-ifp : pstty (ty-ifp Ty2 Ty1) Pst1 (ty-ifp Ty4 Ty3)
  <- appst Pst1 Pst2
  <- pstty Ty1 Pst2 Ty3
  <- pstty Ty2 Pst1 Ty4.
pstty-tag : pstty (ty-tag Ty1 Lst1) Pst (ty-tag Ty2 Lst2)
  <- pstlst Lst1 Pst Lst2
  <- pstty Ty1 Pst Ty2.

astty : ty A1 G E T -> ast A2 A1 -> ty A2 G E T -> type.
%mode astty +Ty1 +Ast -Ty2.
astty-true : astty ty-true Ast ty-true.
astty-false : astty ty-false Ast ty-false.
astty-ifb : astty (ty-ifb Lab Ty3 Ty2 Ty1) Ast (ty-ifb Lab Ty4 Ty5 Ty6)
  <- astty Ty1 Ast Ty4
  <- astty Ty2 Ast Ty5
  <- astty Ty3 Ast Ty6.
astty-var1 : astty ty-var1 Ast ty-var1.
astty-var2 : astty (ty-var2 Ty1) Ast (ty-var2 Ty2)
  <- astty Ty1 Ast Ty2.
astty-fun : astty (ty-fun Ty Ast1) Ast2 (ty-fun Ty (ast-x Ast1 Ast2 Asome))
  <- asome-total Asome.
astty-app : astty (ty-app Ty2 Ty1) Ast (ty-app Ty4 Ty3)
  <- astty Ty1 Ast Ty3
  <- astty Ty2 Ast Ty4.
astty-ifp : astty (ty-ifp Ty2 Ty1) Ast1 (ty-ifp Ty4 Ty3)
  <- apapast Ast1 Ast2
  <- astty Ty1 Ast2 Ty3
  <- astty Ty2 Ast1 Ty4.
astty-tag : astty (ty-tag Ty1 Lst1) Ast (ty-tag Ty2 Lst2)
  <- astlst Lst1 Ast Lst2
  <- astty Ty1 Ast Ty2.

%%\Subhead{Tag checkings}
tyae : ty A gz E T -> ae A E -> type.
%mode tyae +Ty -Ae.
tyae-true : tyae ty-true ae-true.
tyae-false : tyae ty-false ae-false.
tyae-ifb : tyae (ty-ifb Lab Ty3 Ty2 Ty1) (ae-ifb Ae3 Ae2 Ae1)
  <- tyae Ty1 Ae1
  <- tyae Ty2 Ae2
  <- tyae Ty3 Ae3.
tyae-fun : tyae (ty-fun Ty Ast) (ae-fun Ast).
tyae-app : tyae (ty-app Ty2 Ty1) (ae-app Ae2 Ae1)
  <- tyae Ty1 Ae1
  <- tyae Ty2 Ae2.
tyae-ifp : tyae (ty-ifp Ty2 Ty1) (ae-ifp Ae2 Ae1)
  <- tyae Ty1 Ae1
  <- tyae Ty2 Ae2.
tyae-tag : tyae (ty-tag Ty Lst) (ae-tag Ae Lst)
  <- tyae Ty Ae.

aety : ty A1 gz E T -> ae A2 E -> ty A2 gz E T -> type.
%mode aety +Ty1 +Ae -Ty2.
aety-true : aety ty-true ae-true ty-true.
aety-false : aety ty-false ae-false ty-false.
aety-ifb : aety (ty-ifb Lab Ty3 Ty2 Ty1) (ae-ifb Ae3 Ae2 Ae1)
  (ty-ifb Lab Ty6 Ty5 Ty4)
  <- aety Ty1 Ae1 Ty4
  <- aety Ty2 Ae2 Ty5
  <- aety Ty3 Ae3 Ty6. 
aety-fun : aety (ty-fun Ty Ast) (ae-fun Ast2) (ty-fun Ty Ast2).
aety-app : aety (ty-app Ty2 Ty1) (ae-app Ae2 Ae1) (ty-app Ty4 Ty3)
  <- aety Ty1 Ae1 Ty3
  <- aety Ty2 Ae2 Ty4.
aety-ifp : aety (ty-ifp Ty2 Ty1) (ae-ifp Ae2 Ae1) (ty-ifp Ty4 Ty3)
  <- aety Ty1 Ae1 Ty3
  <- aety Ty2 Ae2 Ty4.
aety-tag : aety (ty-tag Ty1 Lst1) (ae-tag Ae Lst2) (ty-tag Ty2 Lst2)
  <- aety Ty1 Ae Ty2.

%%\Subhead{Permutations}
perm : g -> g -> type.
perm-x1 : perm (gx (gx G X1 T1) X2 T2) (gx (gx G X2 T2) X1 T1).
perm-x2 : perm (gx G1 X1 T1) (gx G2 X1 T1)
  <- perm G1 G2.

permty : ty A G1 E T1 -> perm G1 G2 -> ty A G2 E T1 -> type.
%mode permty +Ty1 +Perm -Ty2.
permty-true : permty ty-true Perm ty-true.
permty-false : permty ty-false Perm ty-false.
permty-ifb : permty (ty-ifb Lab Ty3 Ty2 Ty1) Perm (ty-ifb Lab Ty4 Ty5 Ty6)
  <- permty Ty1 Perm Ty4
  <- permty Ty2 Perm Ty5
  <- permty Ty3 Perm Ty6.
permty-var1 : permty ty-var1 Perm ty-var1.
permty-var2 : permty (ty-var2 ty-var1) perm-x1 ty-var1.
permty-var3 : permty (ty-var2 (ty-var2 Ty)) perm-x1 (ty-var2 (ty-var2 Ty)). 
permty-var4 : permty (ty-var2 Ty1) (perm-x2 Perm) (ty-var2 Ty2)
  <- permty Ty1 Perm Ty2.
permty-fun : permty (ty-fun Ty1 Ast) Perm (ty-fun Ty2 Ast)
  <- permty Ty1 (perm-x2 Perm) Ty2.
permty-app : permty (ty-app Ty2 Ty1) Perm (ty-app Ty4 Ty3)
  <- permty Ty1 Perm Ty3
  <- permty Ty2 Perm Ty4.
permty-ifp : permty (ty-ifp Ty2 Ty1) Perm (ty-ifp Ty4 Ty3)
  <- permty Ty1 Perm Ty3
  <- permty Ty2 Perm Ty4.
permty-tag : permty (ty-tag Ty1 Lst) Perm (ty-tag Ty2 Lst)
  <- permty Ty1 Perm Ty2.

%%\Subhead{Substitutions}
subty : ty A (gx G X T1) E1 T2 -> ty az gz E2 T1
  -> sub E1 E2 X E3 -> ty A G E3 T2 -> type. %name subty Subty.
%mode subty +Ty1 +Ty2 +Sub -Ty3.
subty-true : subty ty-true Ty sub-true ty-true.
subty-false : subty ty-false Ty sub-false ty-false.
subty-if : subty (ty-ifb Lab Ty3 Ty2 Ty1) Ty (sub-ifb Sub3 Sub2 Sub1)
  (ty-ifb Lab Ty6 Ty5 Ty4)
  <- subty Ty1 Ty Sub1 Ty4
  <- subty Ty2 Ty Sub2 Ty5
  <- subty Ty3 Ty Sub3 Ty6.
subty-var1 : subty ty-var1 Ty sub-var1 Ty.
subty-var2 : subty (ty-var2 Ty) Ty sub-var2 Ty.
subty-fun : subty (ty-fun Ty1 Ast) Ty (sub-fun Sub) (ty-fun Ty4 Ast)
  <- permty Ty1 perm-x1 Ty2
  <- subty Ty2 Ty Sub Ty4.
subty-app : subty (ty-app Ty2 Ty1) Ty (sub-app Sub2 Sub1) (ty-app Ty4 Ty3)
  <- subty Ty1 Ty Sub1 Ty3
  <- subty Ty2 Ty Sub2 Ty4.

splitty : ty A G E1 T1 -> split E1 Q E2 -> ty A G E2 T2 -> type.
%mode splitty +Ty1 +Split -Ty2.
splitty-ifb : splitty (ty-ifb Lab Ty3 Ty2 Ty1) split-ifb Ty1. 
splitty-app1 : splitty (ty-app Ty2 Ty1) split-app1 Ty1. 
splitty-app2 : splitty (ty-app Ty2 Ty1) split-app2 Ty2. 
splitty-tag : splitty (ty-tag Ty Lst) split-tag Ty. 

combinety : ty A G E1 T1 -> split E1 Q E2 -> ty A G E2 T2 
  -> ty A G E3 T2 -> combine Q E3 E4 -> ty A G E4 T1 -> type.
%mode combinety +Ty1 +Split +Ty2 +Ty3 +Combine -Ty4.
combinety-ifb : combinety (ty-ifb Lab Ty3 Ty2 Ty1) split-ifb Ty1
  Ty4 combine-ifb (ty-ifb Lab Ty3 Ty2 Ty4).
combinety-app1 : combinety (ty-app Ty2 Ty1) split-app1 Ty1
  Ty3 combine-app1 (ty-app Ty2 Ty3).
combinety-app2 : combinety (ty-app Ty2 Ty1) split-app2 Ty2
  Ty3 combine-app2 (ty-app Ty3 Ty1).
combinety-tag : combinety (ty-tag Ty1 Lst) split-tag Ty1
  Ty2 combine-tag (ty-tag Ty2 Lst).


%%\Head{Theorems}
%%\Subhead{Preservation}
valty : ty A G E T -> val E -> ty az gz E T -> type.
%mode valty +Ty1 +Val -Ty2.
valty-true : valty ty-true val-true ty-true.
valty-false : valty ty-false val-false ty-false.
valty-fun : valty (ty-fun Ty Ast) val-fun (ty-fun Ty Ast).

ps : ty A gz E1 T -> ev A E1 E2 -> ty A gz E2 T -> type. %name ps Ps. 
%mode ps +Ty1 +Ev -Ty2.
ps-app : ps (ty-app Ty2 (ty-fun Ty1 Ast)) (ev-app Sub Val) Ty4
  <- valty Ty2 Val Ty3
  <- subty Ty1 Ty3 Sub Ty4.
ps-ifb1 : ps (ty-ifb Lab Ty3 Ty2 Ty1) ev-ifb1 Ty2.
ps-ifb2 : ps (ty-ifb Lab Ty3 Ty2 Ty1) ev-ifb2 Ty3.
ps-ifp1 : ps (ty-ifp Ty2 Ty1) (ev-ifp1 Pst) Ty3
  <- pstty Ty1 Pst Ty3.
ps-ifp2 : ps (ty-ifp Ty2 Ty1) (ev-ifp2 Nlst) Ty2.
ps-tag1 : ps (ty-tag Ty Lst) ev-tag1 ty-true.
ps-tag2 : ps (ty-tag Ty Lst) ev-tag2 ty-false.
ps-hole : ps Ty1 (ev-hole Combine Ev Split) Ty4
  <- splitty Ty1 Split Ty2
  <- ps Ty2 Ev Ty3
  <- combinety Ty1 Split Ty2 Ty3 Combine Ty4.

topps : ty A1 gz E1 T -> topev A1 E1 Ao A2 E2 -> ty A2 gz E2 T -> type. 
%name topps Topps.
%mode topps +Ty1 +Topev -Ty2.
topps-ev : topps Ty1 (topev-ev Ev) Ty2
  <- ps Ty1 Ev Ty2.
topps-upd : topps Ty1 (topev-upd Ae) Ty2
  <- aety Ty1 Ae Ty2.

%%\Subhead{Progress}
ve : a -> e -> type.               
%name ve Ve. 
%mode ve +A +E.
ve-v : ve A E 
  <- val E.
ve-e : ve A E1
  <- ev A E1 E2.

pg : ty A gz E T -> ve A E -> type. 
%name pg Pg.
%mode pg +Ty -Ve.
pg-true : pg ty-true (ve-v val-true).
pg-false : pg ty-false (ve-v val-false).
pg-ifb1 : pg (ty-ifb Lab Ty3 Ty2 Ty1) (ve-e (ev-hole combine-ifb Ev split-ifb))
  <- pg Ty1 (ve-e Ev).
pg-ifb2 : pg (ty-ifb Lab Ty3 Ty2 Ty1) (ve-e ev-ifb1)
  <- pg Ty1 (ve-v Val).
pg-ifb3 : pg (ty-ifb Lab Ty3 Ty2 Ty1) (ve-e ev-ifb2)
  <- pg Ty1 (ve-v Val).
pg-fun : pg (ty-fun Ty Ast) (ve-v val-fun).
pg-app1 : pg (ty-app Ty2 Ty1) (ve-e (ev-hole combine-app1 Ev split-app1))
  <- pg Ty1 (ve-e Ev).
pg-app2 : pg (ty-app Ty2 Ty1) (ve-e (ev-hole combine-app2 Ev split-app2))
  <- pg Ty1 (ve-v Val)
  <- pg Ty2 (ve-e Ev).
pg-app3 : pg (ty-app Ty2 Ty1) (ve-e (ev-app Sub Val2))
  <- pg Ty1 (ve-v Val1)
  <- pg Ty2 (ve-v Val2)
  <- sub-total Sub.
pg-ifp1 : pg (ty-ifp Ty2 Ty1) (ve-e (ev-ifp1 Pst))
  <- pst-total (psty-pst Pst).
pg-ifp2 : pg (ty-ifp Ty2 Ty1) (ve-e (ev-ifp2 Pnst))
  <- pst-total (psty-pnst Pnst).
pg-tag1 : pg (ty-tag Ty Lst) (ve-e ev-tag1)
  <- pg Ty (ve-v Val).
pg-tag2 : pg (ty-tag Ty Lst) (ve-e ev-tag2)
  <- pg Ty (ve-v Val).

topve : a -> e -> type.               
%name topve Topve. 
%mode topve +A +E.
topve-v : topve A E 
  <- val E.
topve-e : topve A1 E1
  <- asome A
  <- topev A1 E1 A A2 E2.

toppg : ty A gz E T -> topve A E -> type.
%mode toppg +Ty -Topve.
toppg-v : toppg Ty (topve-v Val)
  <- pg Ty (ve-v Val).
toppg-e : toppg Ty (topve-e (topev-ev Ev) Asome)
  <- asome-total Asome
  <- pg Ty (ve-e Ev).

%%\Subhead{Soundness}
snd : ty A1 gz E1 T -> bigev A1 E1 A2 E2 -> type.
%mode snd +Ty -Bigev.
snd-v : snd Ty (bigev-v Val)
  <- toppg Ty (topve-v Val).
snd-e : snd Ty1 (bigev-e Bigev Topev Asome)
  <- toppg Ty1 (topve-e Topev Asome)
  <- topps Ty1 Topev Ty2
  <- snd Ty2 Bigev.

%%\Head{Translations}
%%\Subhead{Types}
u : type.                               %name u U.
ubool : l -> u.
ufun : u -> u -> u.

%%\Subhead{Terms}
m : type.                               %name m M.
mtrue : l -> m.
mfalse : l -> m.
mvar : x -> m.
mfun : x -> u -> m -> m.
mapp : m -> m -> m.
mifb : m -> m -> m -> m.
mifl : p -> p -> m -> m -> m.

%%\Subhead{Contexts}
h : type.                               %name h H.
hz : h.
hx : h -> x -> u -> h.


%%\Subhead{Type labels}
ulab : u -> l -> type.
%mode ulab +U -L.
ulab-bool : ulab (ubool L) L.
ulab-fun : ulab (ufun U1 U2) L
  <- ulab U2 L.

%%\Subhead{Subtypings}
ust : a -> u -> u -> type.
%mode ust +A +U1 +U2.
ust-bool : ust A (ubool L1) (ubool L2)
  <- lst A L1 L2.
ust-fun : ust A (ufun U1 U2) (ufun U3 U4)
  <- ust A U3 U1
  <- ust A U2 U4.

%%\Subhead{Typings}
usome : u -> type.
%mode usome -U.

mty : a -> h -> m -> u -> type.
%mode mty +A +H +E -U.
mty-true : mty A H (mtrue L) (ubool L).
mty-false : mty A H (mfalse L) (ubool L).
mty-ifb : mty A H (mifb M1 M2 M3) U
  <- mty A H M1 (ubool L)
  <- mty A H M2 U
  <- mty A H M3 U
  <- ulab U L.
mty-var1 : mty A (hx H X U) (mvar X) U.
mty-var2 : mty A (hx H X1 U1) (mvar X2) U2
  <- mty A H (mvar X2) U2.
mty-fun : mty A H (mfun X U1 M) (ufun U1 U2)
  <- mty A (hx H X U1) M U2.
mty-app : mty A H (mapp M1 M2) U2
  <- mty A H M1 (ufun U1 U2)
  <- mty A H M2 U1.
mty-ifp : mty A H (mifl P1 P2 M1 M2) U
  <- mty (ap A P1 P2) H M1 U
  <- mty A H M2 U.
mty-sub : mty A H M U2 
  <- mty A H M U1
  <- usome U2
  <- ust A U1 U2.

%%\Subhead{Theorems}
ut : u -> t -> type.
%mode ut +U -T.
ut-bool : ut (ubool L) (tbool L).
ut-fun : ut (ufun U1 U2) (tfun T1 T2)
  <- ut U1 T1
  <- ut U2 T2.

ulablab : ulab U L -> ty A G E T -> lab T L -> type.
%mode ulablab +Ulab +Ty -Lab.
ulablab-bool : ulablab ulab-bool Ty lab-bool.
ulablab-fun : ulablab (ulab-fun Ulab) (ty-fun Ty Ast) (lab-fun Lab)
  <- ulablab Ulab Ty Lab.
  
fresh : x -> type.
%mode fresh -X.

ustty : ust A U1 U2 -> ty A G E (tfun T1 T2) -> type.
%mode +{A:a} +{P1:u} +{P2:u} +{G:g} -{E:e} +{T1:t} +{T2:t} +{Ust:ust A P1 P2}
  -{Ty:ty A G E (tfun T1 T2)} (ustty Ust Ty).
ustty-bool : ustty (ust-bool Lst)
  (ty-fun (ty-tag (ty-var1:ty A (gx G X (tbool L1)) (var X) (tbool L1)) Lst)
  ast-z)
  <- fresh X.
ustty-fun : ustty (ust-fun Ust2 Ust1) 
  (ty-fun (ty-fun (ty-app (ty-app (ty-app 
  ty-var1 Ty1) (ty-var2 ty-var1)) Ty2) ast-z) ast-z)
  <- fresh X1
  <- fresh X2
  <- ustty Ust1 (Ty1:ty A (gx (gx G X1 (tfun T1 T2)) X2 T3)
  E1 (tfun T3 T1))
  <- ustty Ust2 Ty2.

mtyty : mty A H M U -> ty A G E T -> type.
%mode +{A:a} +{H:h} +{M:m} +{U:u} +{G:g} -{E:e} -{T:t} +{Mty:mty A H M U}
  -{Ty:ty A G E T} (mtyty Mty Ty).
mtyty-true : mtyty (mty-true:mty A H (mtrue L) (ubool L))
  (ty-true:ty A G (true L) (tbool L)).
mtyty-false : mtyty (mty-false:mty A H (mfalse L) (ubool L))
  (ty-false:ty A G (false L) (tbool L)).
mtyty-if : mtyty (mty-ifb Ulab Mty3 Mty2 Mty1) (ty-ifb Lab Ty3 Ty2 Ty1)
  <- mtyty Mty1 Ty1
  <- mtyty Mty2 Ty2
  <- mtyty Mty3 Ty3
  <- ulablab Ulab Ty1 Lab.
mtyty-var1 : mtyty (mty-var1:mty A (hx H X U) (mvar X) U) 
  (ty-var1:ty A (gx G X T) (var X) T).
mtyty-var2 : mtyty ((mty-var2 Mty):mty A (hx H X1 U1) (mvar X2) U2)
  ((ty-var2 Ty):ty A (gx G X1 T1) (var X2) T2)
  <- mtyty Mty Ty.
mtyty-fun : mtyty (mty-fun (Mty:mty A (hx H X U1) M U2))
  (ty-fun (Ty:ty A (gx G X T1) E T2) ast-z)
  <- ut U1 T1
  <- mtyty Mty Ty.
mtyty-app : mtyty (mty-app Mty2 Mty1) (ty-app Ty2 Ty1)
  <- mtyty Mty1 Ty1
  <- mtyty Mty2 Ty2.
mtyty-ifp : mtyty (mty-ifp Mty2 Mty1) (ty-ifp Ty2 Ty1)
  <- mtyty Mty1 Ty1
  <- mtyty Mty2 Ty2.
mtyty-sub : mtyty (mty-sub (Ust:ust A U1 U2) Usome Mty) 
  (ty-app Ty2 Ty1)
  <- ut U1 T1
  <- ut U2 T2
  <- ustty Ust (Ty1:ty A G E1 (tfun T1 T2))
  <- mtyty Mty Ty2.