%%\Head{Syntax}
%%\Subhead{Kinds}
k : type.                               %name k K.
kt : k.
kl : k.
kp : k.
kj : k.
kpj : k.

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

%%\Subhead{Types}
t : type.                               %name t T.
l = t.
p = t.
j = t.
q = l.
tunit : t.
tprod : t -> t -> t.
tsum : t -> t -> t.
tfun : t -> t -> t.
ttop : t.
tbot : t.
tvar : x -> t.
tall : t -> t -> t.
tsome : t -> t -> t.
tinter : t -> t -> t.
tunion : t -> t -> t.
tlab : t -> l -> t.
teff : t -> q -> t.
tpot : t -> t.
tread : p -> p -> l.
ttrust : p -> l.
tauth : t -> p -> p -> t.
tsin : p -> t.
tcert : t.
tdcls : p -> t.
tendr : t.

%%\Subhead{Terms}
m : type.                               %name m M.
e : type.                               %name e E.
unit : m.
var : x -> m.
prod : m -> m -> m.
prl : m -> m.
prr : m -> m.
inl : m -> t -> m.
inr : m -> t -> m.
case : m -> m -> m -> m.
fun : t -> m -> m.
app : m -> m -> m.
poly : t -> m -> m.
inst : m -> t -> m.
pack : t -> m -> t -> m.
open : m -> m -> m.
lab : m -> l -> m.
bind : m -> m -> m.
eff : e -> q -> m.
fix : m -> m.
lift : m -> m.
seq : m -> m -> m.
let : p -> p -> m -> m.
pass : m -> m -> m.
sin : p -> m.
cert : p -> p -> m.
if : m -> m -> m -> m -> m -> m.

%%\Subhead{Expressions}
ret : m -> e.
run : m -> e -> e.
evar : x -> e.
efix : t -> q -> e -> e.

%%\Subhead{Contexts}
g : type.                               %name g G.
gn : g.
gt : g -> t -> g.
gq : g -> t -> q -> g.

%%\Subhead{Lattices}
d : type.                               %name d D.
dn : d.
dt : d -> t -> d.
dp : d -> p -> p -> d.


%%\Head{Static semantics}
%%\Subhead{Operations}
gtmem : g -> x -> t -> type.
%mode gtmem +G +X -T.
%terminates G (gtmem G X T).

gqmem : g -> x -> t -> q -> type.
%mode gqmem +G +X -T -Q.
%terminates G (gqmem G X T Q).

dtmem : d -> x -> t -> type.
%mode dtmem +G +X -T.
%terminates D (dtmem D X T).

dpmem : d -> p -> p -> type.
%mode dpmem +D -P1 -P2.
%terminates D (dpmem D P1 P2).

mmsub : m -> m -> m -> type.        
%mode mmsub +M1 +M -M2.
%terminates M1 (mmsub M1 M M2).

emsub : e -> m -> e -> type.        
%mode emsub +E1 +M -E2.
%terminates E1 (emsub E1 M E2).

eesub : e -> e -> e -> type.
%mode eesub +E1 +E -E2.
%terminates E1 (eesub E1 E E2).

mtsub : m -> t -> m -> type.         
%mode mtsub +M1 +T -M2.
%terminates M1 (mtsub M1 T M2).

ttsub : t -> t -> t -> type.
%mode ttsub +T1 +T -T2.
%terminates T1 (ttsub T1 T T2).

gindep : g -> type.
%mode gindep +G.
%terminates G (gindep G).

tindep : t -> type.
%mode tindep +T.
%terminates T (tindep T).

%%\Subhead{Kinding}
kd : d -> t -> k -> type.          %name kd Kd.
%mode kd +D +T -K.
kd-unit : kd D tunit kt.
kd-prod : kd D (tprod T1 T2) kt.
kd-sum : kd D (tsum T1 T2) kt.
kd-fun : kd D (tfun T1 T2) kt.
kd-topt : kd D ttop kt.
kd-topl : kd D ttop kl.
kd-topp : kd D ttop kp.
kd-topj : kd D ttop kj.
kd-bott : kd D tbot kt.
kd-botl : kd D tbot kl.
kd-botp : kd D tbot kp.
kd-botj : kd D tbot kj.
kd-all : kd D (tall T1 T2) kt
  <- kd (dt D T1) T2 kt.
kd-some : kd D (tsome T1 T2) kt
  <- kd (dt D T1) T2 kt.
kd-inter : kd D (tinter T1 T2) K
  <- kd D T1 K
  <- kd D T2 K.
kd-union : kd D (tunion T1 T2) K
  <- kd D T1 K
  <- kd D T2 K.
kd-lab : kd D (tlab T L) kt
  <- kd D T kt
  <- kd D L kl.
kd-eff : kd D (teff T Q) kt
  <- kd D T kt
  <- kd D Q kl.
kd-pot : kd D (tpot T) kt
  <- kd D T kt.
kd-read : kd D (tread P1 P2) kl
  <- kd D P1 kp
  <- kd D P2 kp.
kd-trust : kd D (ttrust P) kl
  <- kd D P kp.
kd-auth : kd D (tauth T P1 P2) kt
  <- kd D T kt
  <- kd D P1 kp
  <- kd D P2 kpj.
kd-sin : kd D (tsin T) kt
  <- kd D T K.
kd-cert : kd D tcert kt.
kd-dcls : kd D (tdcls P) kj
  <- kd D P kp.
kd-endr : kd D tendr kj.
%terminates T (kd D T K).
kd-var : kd D (tvar X) K
  <- dtmem D X T
  <- kd D T K.
kd-pjp : kd D T kpj
  <- kd D T kp.
kd-pjj : kd D T kpj
  <- kd D T kj.

%%\Subhead{Subtyping}
st : d -> t -> t -> type.           
stx : d -> t -> t -> type.
nst : d -> t -> t -> type.           
%mode st +D +T1 +T2.
%mode stx +D -T1 -T2.
%mode nst +D +T1 +T2.
st-unit : st D tunit tunit.
st-prod : st D (tprod T1 T2) (tprod T3 T4)
  <- st D T1 T3
  <- st D T2 T4.
st-sum : st D (tsum T1 T2) (tsum T3 T4)
  <- st D T1 T3
  <- st D T2 T4.
st-top : st D T ttop.
st-bot : st D tbot T.
st-var : st D (tvar X) (tvar X).
st-all : st D (tall T T1) (tall T T2)
  <- st (dt D T) T1 T2.
st-some : st D (tsome T T1) (tsome T T2)
  <- st (dt D T) T1 T2.
st-inter1 : st D (tinter T1 T2) T
  <- st D T1 T.
st-inter2 : st D (tinter T1 T2) T
  <- st D T2 T.
st-inter3 : st D T (tinter T1 T2)
  <- st D T T1
  <- st D T T2.
st-union1 : st D T (tunion T1 T2)
  <- st D T T1.
st-union2 : st D T (tunion T1 T2)
  <- st D T T2.
st-union3 : st D (tunion T1 T2) T
  <- st D T1 T
  <- st D T2 T.
st-lab : st D (tlab T1 L1) (tlab T2 L2)
  <- st D T1 T2
  <- st D L1 L2.
st-pot : st D (tpot T1) (tpot T2)
  <- st D T1 T2.
st-read : st D (tread P1 P2) (tread P3 P4)
  <- st D P1 P3
  <- st D P2 P4.
st-sin : st D (tsin T) (tsin T).
st-cert : st D tcert tcert.
st-dcls1 : st D (tdcls T1) (tdcls T2)
  <- st D T1 T2.
st-dcls2 : st D P (tdcls ttop).
st-endr : st D tendr tendr.
st-auth2 : st D T (tauth T P1 P2).
%terminates {T1 T2} (st D T1 T2).

% needs cartsen's tricks to check termination
st-fun : st D (tfun T1 T2) (tfun T3 T4)
  <- st D T3 T1
  <- st D T2 T4.
st-eff : st D (teff T1 Q1) (teff T2 Q2)
  <- st D T1 T2
  <- st D Q2 Q1.
st-read2 : st D (tread P1 P2) (tread P3 P4)
  <- st D P1 P3
  <- stx D P1 (tdcls P)
  <- st D (tinter P P2) P4.
st-trust : st D (ttrust P1) (ttrust P2)
  <- st D P2 P1.
st-trust2 : st D (ttrust P1) (ttrust P2)
  <- stx D P tendr
  <- st D P2 (tunion P P1).
st-auth : st D (tauth T1 P1 P2) (tauth T2 P3 P4)
  <- st D T1 T2
  <- st D P3 P1
  <- st D P2 P4.
st-del : st D P1 P2
  <- dpmem D P1 P2.
%terminates {T1 T2} (nst D T1 T2).


%%\Subhead{Protections}
plab : d -> t -> l -> type.
%mode plab +D +T +L.
plab-unit : plab D tunit L.
plab-prod : plab D (tprod T1 T2) L
  <- plab D T2 L
  <- plab D T1 L.
plab-fun : plab D (tfun T1 T2) L
  <- plab D T2 L.
plab-top : plab D ttop L.
plab-all : plab D (tall T1 T2) L
  <- plab (dt D T1) T2 L.
plab-some : plab D (tsome T1 T2) L
  <- plab (dt D T2) T2 L.
plab-lab1 : plab D (tlab T L1) L2
  <- st D L2 L1.
plab-lab2 : plab D (tlab T L1) L2
  <- nst D L2 L1
  <- plab D T L2.
plab-eff : plab D (teff T Q) L
  <- plab D T L
  <- st D L Q.
plab-pot : plab D (tpot T) L
  <- plab D T L. 
plab-auth : plab D (tauth T P1 P2) (ttrust P)
  <- plab D T (ttrust P)
  <- st D P1 P.
plab-sin : plab D (tsin T) L.
plab-cert : plab D tcert L.
%terminates {T D} (plab D T L).

ppot : d -> t -> type.
%mode ppot +D +T.
%terminates T (ppot D T).
ppot-prod : ppot D (tprod T1 T2)
  <- ppot D T1
  <- ppot D T2.
ppot-sum : ppot D (tsum T1 T2)
  <- ppot D T1
  <- ppot D T2.
ppot-fun : ppot D (tfun T1 T2)
  <- ppot D T2.
ppot-all : ppot D (tall T1 T2)
  <- ppot (dt D T1) T2.
ppot-some : ppot D (tsome T1 T2)
  <- ppot (dt D T1) T2.
ppot-lab : ppot D (tlab T L)
  <- ppot D T.
ppot-eff : ppot D (teff T Q)
  <- ppot D T.
ppot-pot : ppot D (tpot T).
ppot-auth : ppot D (tauth T P1 P2)
  <- ppot D T.


%%\Subhead{Term typings}
ty : d -> g -> m -> t -> type.          %name ty Ty.
tyx : d -> g -> m -> t -> type.          %name tyx Ty.
%mode ty +D +G +M -T.
ety : d -> g -> e -> t -> q -> type.    %name ety Ety.
etyx : d -> g -> e -> t -> q -> type.    %name etyx Ety.
%mode ety +D +G +M -T -Q.

ty-unit : ty D G unit tunit.
ty-prod : ty D G (prod M1 M2) (tprod T1 T2)
  <- ty D G M1 T1
  <- ty D G M2 T2.
ty-prl : ty D G (prl M) T1
  <- ty D G M (tprod T1 T2).
ty-prr : ty D G (prr M) T2
  <- ty D G M (tprod T1 T2).
ty-inl : ty D G (inl M (tsum T1 T2)) (tsum T1 T2)
  <- ty D G M T1
  <- kd D (tsum T1 T2) kt.
ty-inr : ty D G (inr M (tsum T1 T2)) (tsum T1 T2)
  <- ty D G M T2
  <- kd D (tsum T1 T2) kt.
ty-case : ty D G (case M M1 M2) T
  <- ty D G M (tsum T1 T2)
  <- ty D G M1 (tfun T1 T)
  <- ty D G M2 (tfun T2 T).
ty-var : ty D G (var X) T
  <- gtmem G X T.
ty-fun : ty D G (fun T1 M) (tfun T1 T2)
  <- ty D (gt G T1) M T2
  <- kd D T1 kt.
ty-app : ty D G (app M1 M2) T2
  <- ty D G M1 (tfun T1 T2)
  <- ty D G M2 T1.
ty-poly : ty D G (poly T1 M) (tall T1 T2)
  <- ty (dt D T1) G M T2
  <- kd D T1 K
  <- gindep G.
ty-inst : ty D G (inst M T3) T4
  <- ty D G M (tall T1 T2)
  <- kd D T1 K
  <- kd D T3 K
  <- st D T3 T1
  <- ttsub T2 T3 T4.
ty-pack : ty D G (pack T M (tsome T1 T2)) (tsome T1 T2)
  <- kd D T K
  <- kd D T1 K
  <- kd D T2 kt
  <- st D T T1
  <- ttsub T2 T T3
  <- ty D G M T3.
ty-open : ty D G (open M1 M2) T
  <- ty D G M1 (tsome T1 T2)
  <- ty (dt D T1) (gt G T2) M2 T
  <- gindep G
  <- tindep T.
ty-lab : ty D G (lab M L) (tlab T L)
  <- ty D G M T
  <- kd D L kl.
ty-bind : ty D G (bind M1 M2) T2
  <- ty D G M1 (tlab T1 L)
  <- ty D (gt G T1) M2 T2
  <- plab D T2 L.
ty-eff : ty D G (eff E Q) (teff T Q)
  <- ety D G E T Q
  <- kd D Q kl.
ty-fix : ty D G (fix M) T
  <- ty D G M (tfun T T)
  <- ppot D T.
ty-lift : ty D G (lift M) (tpot T)
  <- ty D G M T.
ty-seq : ty D G (seq M1 M2) T2
  <- ty D G M1 (tpot T1)
  <- ty D (gt G T1) M2 T2
  <- ppot D T2.  
ty-let : ty D G (let P1 P2 M) (tauth T P1 P2)
  <- ty (dp D P1 P2) G M T
  <- kd D P1 kp
  <- kd D P2 kpj.
ty-pass : ty D G (pass M1 M2) (tauth T2 P1 P2)
  <- ty D G M1 (tauth T1 P1 P2)
  <- ty (dp D P1 P2) (gt G T1) M2 T2.
ty-sin : ty D G (sin P) (tsin P)
  <- kd D P K.
ty-cert : ty D G (cert P1 P2) tcert
  <- kd D P1 kp
  <- kd D P2 kpj.
ty-if : ty D G (if M1 M2 M3 M4 M5) (tauth T P1 P2)
  <- ty D G M1 tcert
  <- ty D G M2 (tsin P1)
  <- ty D G M3 (tsin P2)
  <- ty (dp D P1 P2) G M4 T
  <- ty D G M5 T
  <- kd D P1 kp
  <- kd D P2 kpj.
%%\label{hack:tyx-sub}
tyx-sub : tyx D G M T2
  <- tyx D G M T1
  <- st D T1 T2.

%%\Subhead{Expression typings}
ety-ret : ety D G (ret M) T ttop
  <- ty D G M T.
ety-run : ety D G (run M E) T2 Q
  <- ty D G M (teff T1 Q)
  <- ety D (gt G T1) E T2 Q.
ety-var : ety D G (evar X) T Q
  <- gqmem G X T Q.
ety-fix : ety D G (efix T Q E) T Q
  <- ety D (gq G T Q) E T Q
  <- ppot D T
  <- kd D Q kl.
%%\label{hack:etyx-sub}
etyx-sub : etyx D G E T2 Q2
  <- etyx D G E T1 Q1
  <- st D T1 T2
  <- st D Q2 Q1.
%terminates (M1 M2) (ty D1 G1 M1 T1) (ety D2 G2 M2 T2 Q2).


%%\Head{Dynamic semantics}
%%\Subhead{Values}
val : m -> type.                        %name val Val.
uval : e -> type.                       %name uval Uval.
%mode val +M.
%mode uval +E.
val-unit : val unit.
val-prod : val (prod M1 M2)
  <- val M1
  <- val M2.
val-inl : val (inl M T)
  <- val M.
val-inr : val (inr M T)
  <- val M.
val-fun : val (fun T M).
val-poly : val (poly T M).
val-pack : val (pack T1 M T2)
  <- val M.
val-lab : val (lab M L)
  <- val M.
val-eff : val (eff M Q).
val-lift : val (lift M)
  <- val M.
val-let : val (let P1 P2 M)
  <- val M.
val-sin : val (sin P).
val-cert : val (cert P1 P2).

uval-ret : uval (ret M)
  <- val M.

%%\Subhead{Verifications}  
ve : p -> p -> p -> p -> type.
%mode ve +P1 +P2 +P3 +P4.
%terminates {} (ve P1 P2 P3 P4).

nve : p -> p -> p -> p -> type.
%mode nve +P1 +P2 +P3 +P4.
%terminates {} (nve P1 P2 P3 P4).


%%\Subhead{Term evaluations}
ev : m -> m -> type.                    %name ev Ev.
%mode ev +M1 -M2.
ev-prod1 : ev (prod M1 M2) (prod M3 M2)
  <- ev M1 M3.
ev-prod2 : ev (prod M1 M2) (prod M2 M3)
  <- val M1
  <- ev M2 M3.
ev-prl1 : ev (prl M1) (prl M2)
  <- ev M1 M2.
ev-prl2 : ev (prl (prod M1 M2)) M1
  <- val M1
  <- val M2.
ev-prr1 : ev (prr M1) (prr M2)
  <- ev M1 M2.
ev-prr2 : ev (prr (prod M1 M2)) M2
  <- val M1
  <- val M2.
ev-inl : ev (inl M1 T) (inl M2 T)
  <- ev M1 M2.
ev-inr : ev (inr M1 T) (inr M2 T)
  <- ev M1 M2.
ev-case1 : ev (case M M1 M2) (case M3 M1 M2)
  <- ev M M3.
ev-case2 : ev (case (inl M T) M1 M2) (app M1 M).
ev-case3 : ev (case (inr M T) M1 M2) (app M2 M).
ev-app1 : ev (app M1 M2) (app M3 M2)
  <- ev M1 M3.
ev-app2 : ev (app M1 M2) (app M1 M3)
  <- val M1
  <- ev M2 M3.
ev-app3 : ev (app (fun T M1) M2) M3
  <- val M2
  <- mmsub M1 M2 M3.
ev-inst1 : ev (inst M1 T) (inst M2 T)
  <- ev M1 M2.
ev-inst2 : ev (inst (poly T1 M1) T2) M2
  <- mtsub M1 T2 M2.
ev-pack : ev (pack T1 M1 T2) (pack T1 M2 T2)
  <- ev M1 M2.
ev-open1 : ev (open M1 M2) (open M3 M2)
  <- ev M1 M3.
ev-open2 : ev (open (pack T1 M1 T2) M2) M4
  <- val M1
  <- mtsub M2 T1 M3
  <- mmsub M3 M1 M4.
ev-lab : ev (lab M1 L) (lab M2 L)
  <- ev M1 M2.
ev-bind1 : ev (bind M1 M2) (bind M3 M2)
  <- ev M1 M3.
ev-bind2 : ev (bind (lab M1 L) M2) M3
  <- val M1
  <- mmsub M2 M1 M3.
ev-fix : ev (fix (fun T M1)) M2
  <- mmsub M1 (fix (fun T M1)) M2.
ev-lift : ev (lift M1) (lift M2)
  <- ev M1 M2.
ev-seq1 : ev (seq M1 M2) (seq M3 M2)
  <- ev M1 M3.
ev-seq2 : ev (seq (lift M1) M2) M3
  <- val M1
  <- mmsub M2 M1 M3.
ev-let : ev (let P1 P2 M1) (let P1 P2 M2)
  <- ev M1 M2.
ev-pass1 : ev (pass M1 M2) (pass M3 M2)
  <- ev M1 M3.
ev-pass2 : ev (pass (let P1 P2 M1) M2) (let P1 P2 M3)
  <- val M1
  <- mmsub M2 M1 M3.
ev-if1 : ev (if M1 M2 M3 M4 M5) (if M6 M2 M3 M4 M5) 
  <- ev M1 M6.
ev-if2 : ev (if M1 M2 M3 M4 M5) (if M1 M6 M3 M4 M5) 
  <- val M1
  <- ev M2 M6.
ev-if3 : ev (if M1 M2 M3 M4 M5) (if M1 M2 M6 M4 M5) 
  <- val M1
  <- val M2
  <- ev M3 M6.
ev-if4 : ev (if (sin P1) (sin P2) (cert P3 P4) M1 M2) (let P1 P2 M1)
  <- ve P1 P2 P3 P4.
ev-if5 : ev (if (sin P1) (sin P2) (cert P3 P4) M1 M2) M2
  <- nve P1 P2 P3 P4.

%%\Subhead{Expression evaluations}
eev : e -> e -> q -> type.                    %name eev Eev.
%mode eev +E1 -E2 -Q.
eev-ret : eev (ret M1) (ret M2) ttop
  <- ev M1 M2.
eev-run1 : eev (run M1 E) (run M2 E) ttop
  <- ev M1 M2.
eev-run2 : eev (run (eff (ret M1) Q) E2) (run (eff (ret M2) Q) E2) ttop
  <- ev M1 M2.
eev-run3 : eev (run (eff (ret M) Q) E1) E2 Q
  <- val M
  <- emsub E1 M E2.
eev-fix : eev (efix T Q E1) E2 ttop
  <- eesub E1 (efix T Q E1) E2. 

%%\Head{Soundness}
%%\Subhead{Evaluation or value}
evval : m -> type.                      %name evval Evval. 
%mode evval +M.
evval-ev : evval M1
  <- ev M1 M2.
evval-val : evval M 
  <- val M.

eevuval : e -> type.                      %name eevuval Eevuval. 
%mode eevuval +E.
eevuval-eev : eevuval E1
  <- eev E1 E2 Q.
eevuval-uval : eevuval E 
  <- uval E.

%%\Subhead{Function totality}
subx : mmsub M1 M2 M3 -> type.
%mode +{M1:m} +{M2:m} +{X:x} -{M3:m} -{Mmsub:mmsub M1 M2 M3} (subx Mmsub).
%terminates {} (subx Mmsub).

mtsubx : mtsub M1 T M2 -> type.
%mode +{M1:m} +{T:t} +{X:x} -{M2:m} -{Mtsub:mtsub M1 T M2} (mtsubx Mtsub).
%terminates {} (mtsubx Mtsub).

emsubx : emsub E1 M E2 -> type.
%mode +{E1:e} +{M:m} +{X:x} -{E2:e} -{Emsub:emsub E1 M E2} (emsubx Emsub).
%terminates {} (emsubx Emsub).

eesubx : eesub E1 E E2 -> type.
%mode +{E1:e} +{E:e} +{X:x} -{E2:e} -{Eesub:eesub E1 E E2} (eesubx Eesub).
%terminates {} (eesubx Eesub).

venve : p -> p -> p -> p -> type.
%mode venve +P1 +P2 +P3 +P4.
%terminates {} (ve P1 P2 P3 P4).
venve-ve : venve P1 P2 P3 P4
  <- ve P1 P2 P3 P4.
venve-nve : venve P1 P2 P3 P4
  <- nve P1 P2 P3 P4.

vex : venve P1 P2 P3 P4 -> type.
%mode vex -Venve.
%terminates {} (vex Venve).

%%\Subhead{Term progress}
pg : ty D gn M T -> evval M -> type.    %name pg Pg.
%mode pg +Ty -Evval.
pg-unit : pg ty-unit (evval-val val-unit).
pg-prod1 : pg (ty-prod Ty2 Ty1) (evval-ev (ev-prod1 Ev))
  <- pg Ty1 (evval-ev Ev).
pg-prod2 : pg (ty-prod Ty2 Ty1) (evval-ev (ev-prod2 Ev Val))
  <- pg Ty1 (evval-val Val)
  <- pg Ty2 (evval-ev Ev).
pg-prod3 : pg (ty-prod Ty2 Ty1) (evval-val (val-prod Val2 Val1))
  <- pg Ty1 (evval-val Val1)
  <- pg Ty2 (evval-val Val2).
pg-prl1 : pg (ty-prl Ty) (evval-ev (ev-prl1 Ev))
  <- pg Ty (evval-ev Ev).
pg-prl2 : pg (ty-prl Ty) (evval-ev (ev-prl2 Val2 Val1))
  <- pg Ty (evval-val (val-prod Val2 Val1)).
pg-prr1 : pg (ty-prr Ty) (evval-ev (ev-prr1 Ev))
  <- pg Ty (evval-ev Ev).
pg-prr2 : pg (ty-prr Ty) (evval-ev (ev-prr2 Val2 Val1))
  <- pg Ty (evval-val (val-prod Val2 Val1)).
pg-fun : pg (ty-fun Kd Ty)  (evval-val val-fun).
pg-app1 : pg (ty-app Ty2 Ty1) (evval-ev (ev-app1 Ev))
  <- pg Ty1 (evval-ev Ev).
pg-app2 : pg (ty-app Ty2 Ty1) (evval-ev (ev-app2 Ev Val))
  <- pg Ty1 (evval-val Val)
  <- pg Ty2 (evval-ev Ev).
pg-app3 : pg (ty-app Ty2 (ty-fun Kd Ty1)) 
  (evval-ev (ev-app3 Mmsub Val))
  <- subx Mmsub
  <- pg Ty2 (evval-val Val).
pg-poly : pg (ty-poly Gindep Kd Ty) (evval-val val-poly).
pg-inst1 : pg (ty-inst Ttsub St Kd2 Kd1 Ty) (evval-ev (ev-inst1 Ev))
  <- pg Ty (evval-ev Ev).
pg-inst2 : pg (ty-inst Ttsub St Kd1 Kd2 (ty-poly Gindep Kd3 Ty)) 
  (evval-ev (ev-inst2 Mtsub))
  <- mtsubx Mtsub.
pg-pack1 : pg (ty-pack Ty Ttsub St Kd3 Kd2 Kd1) (evval-ev (ev-pack Ev))
  <- pg Ty (evval-ev Ev).
pg-pack2 : pg (ty-pack Ty Ttsub St Kd3 Kd2 Kd1) (evval-val (val-pack Val))
  <- pg Ty (evval-val Val).
pg-open1 : pg (ty-open Tindep Gindep Ty2 Ty1) (evval-ev (ev-open1 Ev))
  <- pg Ty1 (evval-ev Ev).
pg-open2 : pg (ty-open Tindep Gindep Ty2 Ty1) 
  (evval-ev (ev-open2 Mmsub Mtsub Val))
  <- pg Ty1 (evval-val (val-pack Val))
  <- mtsubx Mtsub
  <- subx Mmsub.
pg-lab1 : pg (ty-lab Kd Ty) (evval-ev (ev-lab Ev))
  <- pg Ty (evval-ev Ev).
pg-lab2 : pg (ty-lab Kd Ty) (evval-val (val-lab Val))
  <- pg Ty (evval-val Val).
pg-bind1 : pg (ty-bind Plab Ty2 Ty1) (evval-ev (ev-bind1 Ev))
  <- pg Ty1 (evval-ev Ev).
pg-bind2 : pg (ty-bind Plab Ty2 Ty1) (evval-ev (ev-bind2 Mmsub Val))
  <- subx Mmsub
  <- pg Ty1 (evval-val (val-lab Val)).
pg-eff : pg (ty-eff Kd Ety) (evval-val val-eff).
pg-fix : pg (ty-fix Ppot Ty) (evval-ev (ev-fix Mmsub))
  <- subx Mmsub.
pg-lift1 : pg (ty-lift Ty) (evval-ev (ev-lift Ev))
  <- pg Ty (evval-ev Ev).
pg-lift2 : pg (ty-lift Ty) (evval-val (val-lift Val))
  <- pg Ty (evval-val Val).
pg-seq1 : pg (ty-seq Ppot Ty2 Ty1) (evval-ev (ev-seq1 Ev))
  <- pg Ty1 (evval-ev Ev).
pg-seq2 : pg (ty-seq Ppot Ty2 Ty1) (evval-ev (ev-seq2 Mmsub Val))
  <- pg Ty1 (evval-val (val-lift Val))
  <- subx Mmsub.
pg-let1 : pg (ty-let Kd2 Kd1 Ty) (evval-ev (ev-let Ev))
  <- pg Ty (evval-ev Ev).
pg-let2 : pg (ty-let Kd2 Kd1 Ty) (evval-val (val-let Val))
  <- pg Ty (evval-val Val).
pg-pass1 : pg (ty-pass Ty2 Ty1) (evval-ev (ev-pass1 Ev))
  <- pg Ty1 (evval-ev Ev).
pg-pass2 : pg (ty-pass Ty2 Ty1) (evval-ev (ev-pass2 Mmsub Val))
  <- pg Ty1 (evval-val (val-let Val))
  <- subx Mmsub.
pg-sin : pg (ty-sin Kd) (evval-val val-sin).
pg-cert : pg (ty-cert Kd2 Kd1) (evval-val val-cert).
pg-if1 : pg (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty2 Ty1) (evval-ev (ev-if1 Ev))
  <- pg Ty1 (evval-ev Ev).
pg-if2 : pg (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty2 Ty1) (evval-ev (ev-if2 Ev Val))
  <- pg Ty1 (evval-val Val)
  <- pg Ty2 (evval-ev Ev).
pg-if3 : pg (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty2 Ty1) 
  (evval-ev (ev-if3 Ev Val2 Val1))
  <- pg Ty1 (evval-val Val1)
  <- pg Ty2 (evval-val Val2)
  <- pg Ty3 (evval-ev Ev).
pg-if4 : pg (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty2 Ty1) (evval-ev (ev-if4 Ve))
  <- pg Ty1 (evval-val Val1)
  <- pg Ty2 (evval-val Val2)
  <- pg Ty3 (evval-val Val3)
  <- vex (venve-ve Ve). 
pg-if5 : pg (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty2 Ty1) (evval-ev (ev-if5 Nve))
  <- pg Ty1 (evval-val Val1)
  <- pg Ty2 (evval-val Val2)
  <- pg Ty3 (evval-val Val3)
  <- vex (venve-nve Nve). 

%%\Subhead{Expression progress}
epg : ety D gn E T Q -> eevuval E -> type. %name epg Epg.
%mode epg +Ety -Eevuval.
epg-ret1 : epg (ety-ret Ty) (eevuval-eev (eev-ret Ev))
  <- pg Ty (evval-ev Ev).
epg-ret2 : epg (ety-ret Ty) (eevuval-uval (uval-ret Val))
  <- pg Ty (evval-val Val).
epg-run1 : epg (ety-run Ety Ty) (eevuval-eev (eev-run1 Ev))
  <- pg Ty (evval-ev Ev).
epg-run2 : epg (ety-run Ety (ty-eff Kd (ety-ret Ty)))
  (eevuval-eev (eev-run2 Ev))
  <- pg Ty (evval-ev Ev).
epg-run3 : epg (ety-run Ety (ty-eff Kd (ety-ret Ty)))
  (eevuval-eev (eev-run3 Emsub Val))
  <- pg Ty (evval-val Val)
  <- emsubx Emsub.
epg-fix : epg (ety-fix Kd Ppot Ety) (eevuval-eev (eev-fix Eesub))
  <- eesubx Eesub.
%terminates Ty (pg Ty Evval).
%terminates Ety (epg Ety Eevuval).

%%\Subhead{Lemmas}
pssub : ty D (gt G T1) M1 T2 -> ty D G M2 T1 -> mmsub M1 M2 M3 
  -> ty D G M3 T2 -> type.
%mode pssub +Ty1 +Ty2 +Sub -Ty3.
%terminates Ty1 (pssub Ty1 Ty2 Mmsub Ty3). 

psemsub : ety D (gt G T1) E1 T2 Q -> ty D G M T1 -> emsub E1 M E2 
  -> ety D G E2 T2 Q -> type.
%mode psemsub +Ety1 +Ety2 +Emsub -Ety3.
%terminates Ety1 (psemsub Ety1 Ety2 Emsub Ety3). 

pseesub : ety D (gq G Q T1) E1 T2 Q -> ety D G E2 T1 Q -> eesub E1 E2 E3
  -> ety D G E3 T2 Q -> type.
%mode pseesub +Ety1 +Ety2 +Eesub -Ety3.
%terminates Ety1 (pseesub Ety1 Ety2 Eesub Ety3). 

psmtsub1 : ty (dt D T1) G M1 T2 -> st D T T1 
  -> gindep G -> mtsub M1 T M2 -> ttsub T2 T T3
  -> ty D G M2 T3 -> type.
%mode psmtsub1 +Ty1 +Mt +Gindep +Mtsub +Ttsub -Ty2.
%terminates Ty1 (psmtsub1 Ty1 St Gindep Mtsub Ttsub Ty2). 

psmtsub2 : ty (dt D T1) (gt G T2) M1 T3 -> st D T T1
  -> gindep G -> ttsub T2 T T4
  -> mtsub M1 T M2 -> tindep T3
  -> ty D (gt G T4) M2 T3 -> type.
%mode psmtsub2 +Ty1 +St +Gindep +Ttsub +Mtsub +Tindep -Ty2.
%terminates Ty1 (psmtsub2 Ty1 St Gindep Ttsub Mtsub Tindep Ty2). 

%%\label{hack:psst}
psst : ty D G M T1 -> st D T1 T2 -> ty D G M T2 -> type.
%mode psst +Ty1 +St -Ty2. 
%terminates Ty1 (psst Ty1 St Ty2).

%%\label{hack:stinv}
stinv : ety D G (ret M) T Q -> ety D G (ret M) T ttop -> type.
%mode stinv +Ety1 -Ety2. 
%terminates Ety1 (stinv Ety1 Ety2).


%%\Subhead{Term preservation}
ps : ty D G M1 T -> ev M1 M2 -> ty D G M2 T -> type. %name ps Ps. 
%mode ps +Ty1 +Ev -Ty2.
ps-prod1 : ps (ty-prod Ty2 Ty1) (ev-prod1 Ev) (ty-prod Ty2 Ty3)
  <- ps Ty1 Ev Ty3.
ps-prod2 : ps (ty-prod Ty2 Ty1) (ev-prod2 Ev Val) (ty-prod Ty3 Ty1)
  <- ps Ty2 Ev Ty3.
ps-prl1 : ps (ty-prl Ty1) (ev-prl1 Ev) (ty-prl Ty2)
  <- ps Ty1 Ev Ty2.
ps-prl2 : ps (ty-prl (ty-prod Ty2 Ty1)) (ev-prl2 Val2 Val1) Ty1.
ps-prr1 : ps (ty-prr Ty1) (ev-prr1 Ev) (ty-prr Ty2)
  <- ps Ty1 Ev Ty2.
ps-prr2 : ps (ty-prr (ty-prod Ty2 Ty1)) (ev-prr2 Val2 Val1) Ty2.
ps-inl : ps (ty-inl Kd Ty1) (ev-inl Ev) (ty-inl Kd Ty2)
  <- ps Ty1 Ev Ty2.
ps-inr : ps (ty-inr Kd Ty1) (ev-inr Ev) (ty-inr Kd Ty2)
  <- ps Ty1 Ev Ty2.
ps-case1 : ps (ty-case Ty3 Ty2 Ty1) (ev-case1 Ev) (ty-case Ty3 Ty2 Ty4)
  <- ps Ty1 Ev Ty4.
ps-case2 : ps (ty-case Ty3 Ty2 (ty-inl Kd Ty1)) 
  ev-case2 (ty-app Ty1 Ty2).
ps-case3 : ps (ty-case Ty3 Ty2 (ty-inr Kd Ty1)) 
  ev-case3 (ty-app Ty1 Ty3).
ps-app1 : ps (ty-app Ty2 Ty1) (ev-app1 Ev) (ty-app Ty2 Ty3)
  <- ps Ty1 Ev Ty3.
ps-app2 : ps (ty-app Ty2 Ty1) (ev-app2 Ev Val) (ty-app Ty3 Ty1)
  <- ps Ty2 Ev Ty3.
ps-app3 : ps (ty-app Ty2 (ty-fun Kd Ty3)) (ev-app3 Mmsub Val) Ty4
 <- pssub Ty3 Ty2 Mmsub Ty4.
ps-inst1 : ps (ty-inst Ttsub St Kd2 Kd1 Ty1) (ev-inst1 Ev) 
  (ty-inst Ttsub St Kd2 Kd1 Ty2)
  <- ps Ty1 Ev Ty2.
ps-inst2 : ps (ty-inst Ttsub St Kd2 Kd1 (ty-poly Gindep Kd3 Ty2)) 
  (ev-inst2 Mtsub) Ty3
  <- psmtsub1 Ty2 St Gindep Mtsub Ttsub Ty3.
ps-pack : ps (ty-pack Ty1 Ttsub St Kd3 Kd2 Kd1) (ev-pack Ev)
  (ty-pack Ty2 Ttsub St Kd3 Kd2 Kd1)
  <- ps Ty1 Ev Ty2.
ps-open1 : ps (ty-open Tindep Gindep Ty2 Ty1) (ev-open1 Ev) 
  (ty-open Tindep Gindep Ty2 Ty3)
  <- ps Ty1 Ev Ty3.
ps-open2 : ps (ty-open Tindep Gindep Ty2 (ty-pack Ty1 Ttsub St Kd3 Kd2 Kd1))
  (ev-open2 Mmsub Mtsub Val) Ty4
  <- psmtsub2 Ty2 St Gindep Ttsub Mtsub Tindep Ty3
  <- pssub Ty3 Ty1 Mmsub Ty4.
ps-lab : ps (ty-lab Kd Ty1) (ev-lab Ev) (ty-lab Kd Ty2)
  <- ps Ty1 Ev Ty2.
ps-bind1 : ps (ty-bind Plab Ty2 Ty1) (ev-bind1 Ev) (ty-bind Plab Ty2 Ty3)
  <- ps Ty1 Ev Ty3.
ps-bind2 : ps (ty-bind Plab Ty2 (ty-lab Kd Ty1)) (ev-bind2 Mmsub Val) Ty3
  <- pssub Ty2 Ty1 Mmsub Ty3.
ps-fix : ps (ty-fix Ppot (ty-fun Kd Ty1)) (ev-fix Mmsub) Ty2
  <- pssub Ty1 (ty-fix Ppot (ty-fun Kd Ty1)) Mmsub Ty2.
ps-lift : ps (ty-lift Ty1) (ev-lift Ev) (ty-lift Ty2)
  <- ps Ty1 Ev Ty2.
ps-seq1 : ps (ty-seq Ppot Ty2 Ty1) (ev-seq1 Ev) (ty-seq Ppot Ty2 Ty3)
  <- ps Ty1 Ev Ty3.
ps-seq2 : ps (ty-seq Ppot Ty2 (ty-lift Ty1)) (ev-seq2 Mmsub Val) Ty3
  <- pssub Ty2 Ty1 Mmsub Ty3.
ps-let : ps (ty-let Kd2 Kd1 Ty1) (ev-let Ev) (ty-let Kd2 Kd1 Ty2)
  <- ps Ty1 Ev Ty2.
ps-pass1 : ps (ty-pass Ty2 Ty1) (ev-pass1 Ev) (ty-pass Ty2 Ty3)
  <- ps Ty1 Ev Ty3.
ps-pass2 : ps (ty-pass Ty2 (ty-let Kd2 Kd1 Ty1)) (ev-pass2 Mmsub Val) 
  (ty-let Kd2 Kd1 Ty3)
  <- pssub Ty2 Ty1 Mmsub Ty3.
ps-if1 : ps (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty2 Ty1) (ev-if1 Ev) 
  (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty2 Ty6)
  <- ps Ty1 Ev Ty6.
ps-if2 : ps (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty2 Ty1) (ev-if2 Ev Val) 
  (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty6 Ty1)
  <- ps Ty2 Ev Ty6.
ps-if3 : ps (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty2 Ty1) (ev-if3 Ev Val2 Val1) 
  (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty6 Ty1)
  <- ps Ty3 Ev Ty6.
ps-if4 : ps (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty2 Ty1) (ev-if4 Ve) 
  (ty-let Kd2 Kd1 Ty4).
%%\label{hack:ps-if5}
ps-if5 : ps (ty-if Kd2 Kd1 Ty5 Ty4 Ty3 Ty2 Ty1) (ev-if5 Nve) Ty6
  <- psst Ty5 st-auth2 Ty6.
%terminates Ev (ps Ty1 Ev Ty2).

%%\Subhead{Expression preservation}
eps : ety D G E1 T Q1 -> eev E1 E2 Q2 -> ety D G E2 T Q1 -> type. %name eps Eps. 
%mode eps +Ety1 +Eev -Ety2.
eps-ret : eps (ety-ret Ty1) (eev-ret Ev) (ety-ret Ty2)
  <- ps Ty1 Ev Ty2.
eps-run1 : eps (ety-run Ety Ty1) (eev-run1 Ev) (ety-run Ety Ty2)
  <- ps Ty1 Ev Ty2.
eps-run2 : eps (ety-run Ety (ty-eff Kd (ety-ret Ty1))) (eev-run2 Ev) 
  (ety-run Ety (ty-eff Kd (ety-ret Ty2)))
  <- ps Ty1 Ev Ty2.
%%\label{hack:eps-run3}
eps-run3 : eps (ety-run Ety1 (ty-eff Kd Ety))
  (eev-run3 Emsub Val) Ety2
  <- stinv Ety (ety-ret Ty1)
  <- psemsub Ety1 Ty1 Emsub Ety2.
eps-fix : eps (ety-fix Ppot Kd Ety1) (eev-fix Eesub) Ety2
  <- pseesub Ety1 (ety-fix Ppot Kd Ety1) Eesub Ety2.
%terminates Eev (eps Ety1 Eev Ety2).