Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/23781ba1f02ec25cd76458f6614433c7]
uninhabited : type.
fluid : type.
fluids : type.
# : fluids.
, : fluid -> fluids -> fluids.
%infix right 10 ,.
a : fluid.
b : fluid.
c : fluid.
d : fluid.
%block bfluid : block {f:fluid}.
eqfluid : fluid -> fluid -> type.
eqfluid/refl : {A:fluid} eqfluid A A.
neqfluid : fluid -> fluid -> type.
neqfluid/ab : neqfluid a b.
neqfluid/ac : neqfluid a c.
neqfluid/ad : neqfluid a d.
neqfluid/ba : neqfluid b a.
neqfluid/bc : neqfluid b c.
neqfluid/bd : neqfluid b d.
neqfluid/ca : neqfluid c a.
neqfluid/cb : neqfluid c b.
neqfluid/cd : neqfluid c d.
neqfluid/da : neqfluid d a.
neqfluid/db : neqfluid d b.
neqfluid/dc : neqfluid d c.
decidable-fluid : fluid -> fluid -> type.
decidable-fluid/eq : {A:fluid} decidable-fluid A A.
decidable-fluid/neq : {A:fluid} {B:fluid} neqfluid A B -> decidable-fluid A B.
eq-or-neq-total : {A:fluid} {B:fluid} decidable-fluid A B -> type.
- : eq-or-neq-total a a decidable-fluid/eq.
- : eq-or-neq-total a b (decidable-fluid/neq neqfluid/ab).
- : eq-or-neq-total a c (decidable-fluid/neq neqfluid/ac).
- : eq-or-neq-total a d (decidable-fluid/neq neqfluid/ad).
- : eq-or-neq-total b a (decidable-fluid/neq neqfluid/ba).
- : eq-or-neq-total b b decidable-fluid/eq.
- : eq-or-neq-total b c (decidable-fluid/neq neqfluid/bc).
- : eq-or-neq-total b d (decidable-fluid/neq neqfluid/bd).
- : eq-or-neq-total c a (decidable-fluid/neq neqfluid/ca).
- : eq-or-neq-total c b (decidable-fluid/neq neqfluid/cb).
- : eq-or-neq-total c c decidable-fluid/eq.
- : eq-or-neq-total c d (decidable-fluid/neq neqfluid/cd).
- : eq-or-neq-total d a (decidable-fluid/neq neqfluid/da).
- : eq-or-neq-total d b (decidable-fluid/neq neqfluid/db).
- : eq-or-neq-total d c (decidable-fluid/neq neqfluid/dc).
- : eq-or-neq-total d d decidable-fluid/eq.
%mode +{A:fluid} +{B:fluid} -{D:decidable-fluid A B} (eq-or-neq-total A B D).
%worlds () (eq-or-neq-total _ _ _).
%total {} (eq-or-neq-total _ _ _).
exclusive-fluid :
   {A:fluid} {B:fluid} eqfluid A B -> neqfluid A B -> uninhabited -> type.
%mode +{A:fluid} +{B:fluid} +{A1:eqfluid A B} +{B1:neqfluid A B} -{C:uninhabited}
   (exclusive-fluid A1 B1 C).
%worlds () (exclusive-fluid _ _ _).
%total {} (exclusive-fluid _ _ _).
in : fluid -> fluids -> type.
in/z : {A:fluid} {As:fluids} in A (A , As).
in/s : {A:fluid} {As:fluids} {B:fluid} in A As -> in A (B , As).
subset : fluids -> fluids -> type.
subset/z : {As:fluids} subset # As.
subset/s :
   {A:fluid} {Bs:fluids} {As:fluids}
      in A Bs -> subset As Bs -> subset (A , As) Bs.
merge : fluids -> fluids -> fluids -> type.
merge/z : {Bs:fluids} merge # Bs Bs.
merge/s :
   {As:fluids} {Bs:fluids} {Cs:fluids} {A:fluid}
      merge As Bs Cs -> merge (A , As) Bs (A , Cs).
in-subset :
   {A:fluid} {Bs:fluids} {Cs:fluids} in A Bs -> subset Bs Cs -> in A Cs -> type.
- :
   {A:fluid} {Bs:fluids} {Cs:fluids} {In:in A Cs} {Sub:subset Bs Cs}
      in-subset in/z (subset/s In Sub) In.
- :
   {A:fluid} {Bs:fluids} {Cs:fluids} {In:in A Bs} {Sub:subset Bs Cs}
      {In'':in A Cs} {B:fluid} {In':in B Cs}
      in-subset In Sub In'' -> in-subset (in/s In) (subset/s In' Sub) In''.
%mode +{A:fluid} +{Bs:fluids} +{Cs:fluids} +{A1:in A Bs} +{B:subset Bs Cs}
   -{C:in A Cs} (in-subset A1 B C).
%worlds (bfluid) (in-subset _ _ _).
%total T (in-subset T _ _).
in-merge1 :
   {A:fluid} {As:fluids} {Bs:fluids} {Cs:fluids}
      in A As -> merge As Bs Cs -> in A Cs -> type.
- :
   {X1:fluid} {X2:fluids} {X3:fluids} {X4:fluids} {X5:merge X2 X3 X4}
      in-merge1 in/z (merge/s X5) in/z.
- :
   {X1:fluid} {X2:fluids} {X3:fluids} {X4:fluids} {In:in X1 X2}
      {Merge:merge X2 X3 X4} {In':in X1 X4} {X5:fluid}
      in-merge1 In Merge In' -> in-merge1 (in/s In) (merge/s Merge) (in/s In').
%mode +{A:fluid} +{As:fluids} +{Bs:fluids} +{Cs:fluids} +{A1:in A As}
   +{B:merge As Bs Cs} -{C:in A Cs} (in-merge1 A1 B C).
%worlds () (in-merge1 _ _ _).
%total T (in-merge1 _ T _).
in-merge2 :
   {A:fluid} {Bs:fluids} {As:fluids} {Cs:fluids}
      in A Bs -> merge As Bs Cs -> in A Cs -> type.
- : {X1:fluid} {X2:fluids} {In:in X1 X2} in-merge2 In merge/z In.
- :
   {X1:fluid} {X2:fluids} {X3:fluids} {X4:fluids} {In:in X1 X2}
      {Merge:merge X3 X2 X4} {In':in X1 X4} {X5:fluid}
      in-merge2 In Merge In' -> in-merge2 In (merge/s Merge) (in/s In').
%mode +{A:fluid} +{Bs:fluids} +{As:fluids} +{Cs:fluids} +{A1:in A Bs}
   +{B:merge As Bs Cs} -{C:in A Cs} (in-merge2 A1 B C).
%worlds () (in-merge2 _ _ _).
%total T (in-merge2 _ T _).
eq-or-in : fluid -> fluid -> fluids -> type.
eq-or-in/eq : {A:fluid} {Cs:fluids} eq-or-in A A Cs.
eq-or-in/in : {A:fluid} {Cs:fluids} {B:fluid} in A Cs -> eq-or-in A B Cs.
in-inversion :
   {A:fluid} {B:fluid} {Cs:fluids} in A (B , Cs) -> eq-or-in A B Cs -> type.
- : {X1:fluid} {X2:fluids} in-inversion in/z eq-or-in/eq.
- :
   {X1:fluid} {X2:fluid} {X3:fluids} {Sub:in X1 X3}
      in-inversion (in/s Sub) (eq-or-in/in Sub).
%mode +{A:fluid} +{B:fluid} +{Cs:fluids} +{A1:in A (B , Cs)} -{B1:eq-or-in A B Cs}
   (in-inversion A1 B1).
%worlds (bfluid) (in-inversion _ _).
%total {} (in-inversion _ _).
subset-trans :
   {As:fluids} {Bs:fluids} {Cs:fluids}
      subset As Bs -> subset Bs Cs -> subset As Cs -> type.
- : {X1:fluids} {X2:fluids} {X3:subset X1 X2} subset-trans subset/z X3 subset/z.
- :
   {FS:fluids} {HS:fluids} {Sub:subset FS HS} {Sub':subset HS HS}
      {Sub'':subset FS HS} {X1:fluid} {In:in X1 HS}
      subset-trans Sub Sub' Sub''
         -> subset-trans (subset/s In Sub) Sub' (subset/s In Sub'').
- :
   {A:fluid} {Bs:fluids} {Cs:fluids} {In:in A Bs} {Sub':subset Bs Cs}
      {In':in A Cs} {As:fluids} {Sub:subset As Bs} {Sub'':subset As Cs}
      in-subset In Sub' In' -> subset-trans Sub Sub' Sub''
         -> subset-trans (subset/s In Sub) Sub' (subset/s In' Sub'').
%mode +{As:fluids} +{Bs:fluids} +{Cs:fluids} +{FG:subset As Bs} +{GH:subset Bs Cs}
   -{FH:subset As Cs} (subset-trans FG GH FH).
%worlds (bfluid) (subset-trans _ _ _).
%total T (subset-trans T _ _).
subset-weaken :
   {Bs:fluids} {Cs:fluids} {C:fluid} subset Bs Cs -> subset Bs (C , Cs) -> type.
- : {X1:fluids} {C:fluid} subset-weaken C subset/z subset/z.
- :
   {Bs:fluids} {Cs:fluids} {C:fluid} {Sub:subset Bs Cs}
      {Sub':subset Bs (C , Cs)} {B:fluid} {In:in B Cs}
      subset-weaken C Sub Sub'
         -> subset-weaken C (subset/s In Sub) (subset/s (in/s In) Sub').
%mode +{Bs:fluids} +{Cs:fluids} +{A:fluid} +{AS:subset Bs Cs}
   -{Sub:subset Bs (A , Cs)} (subset-weaken A AS Sub).
%worlds (bfluid) (subset-weaken _ _ _).
%total T (subset-weaken _ T _).
subset-refl : {FS:fluids} subset FS FS -> type.
- : subset-refl # subset/z.
- :
   {As:fluids} {A:fluid} {Sub:subset As As} {Sub':subset As (A , As)}
      subset-weaken A Sub Sub' -> subset-refl As Sub
         -> subset-refl (A , As) (subset/s in/z Sub').
%mode +{As:fluids} -{S:subset As As} (subset-refl As S).
%worlds (bfluid) (subset-refl _ _).
%total T (subset-refl T _).
merge-subset1 :
   {As:fluids} {Bs:fluids} {Cs:fluids} merge As Bs Cs -> subset As Cs -> type.
- : {X1:fluids} merge-subset1 merge/z subset/z.
- :
   {As:fluids} {Cs:fluids} {A:fluid} {Sub:subset As Cs}
      {Sub':subset As (A , Cs)} {Bs:fluids} {Merge:merge As Bs Cs}
      subset-weaken A Sub Sub' -> merge-subset1 Merge Sub
         -> merge-subset1 (merge/s Merge) (subset/s in/z Sub').
%mode +{As:fluids} +{Bs:fluids} +{Cs:fluids} +{A:merge As Bs Cs} -{B:subset As Cs}
   (merge-subset1 A B).
%worlds (bfluid) (merge-subset1 _ _).
%total T (merge-subset1 T _).
ty : type.
ty/nat : ty.
ty/arrow : ty -> ty -> ty.
ty/mayuse : ty -> fluids -> ty.
eqty : ty -> ty -> type.
eqty/refl : {T:ty} eqty T T.
fluidty : fluid -> ty -> type.
%block ftyblock : some {T:ty} block {f:fluid} {d:fluidty f T}.
fluidty/a : fluidty a ty/nat.
fluidty/b : fluidty b (ty/arrow ty/nat (ty/mayuse ty/nat (a , c , #))).
fluidty/c : fluidty c ty/nat.
fluidty/d : fluidty d (ty/arrow ty/nat ty/nat).
fluidty-uniq :
   {A:fluid} {T:ty} {T':ty} fluidty A T -> fluidty A T' -> eqty T T' -> type.
- : fluidty-uniq fluidty/a fluidty/a eqty/refl.
- : fluidty-uniq fluidty/b fluidty/b eqty/refl.
- : fluidty-uniq fluidty/c fluidty/c eqty/refl.
- : fluidty-uniq fluidty/d fluidty/d eqty/refl.
%mode +{A:fluid} +{T:ty} +{T':ty} +{A1:fluidty A T} +{B:fluidty A T'} -{C:eqty T T'}
   (fluidty-uniq A1 B C).
%worlds () (fluidty-uniq _ _ _).
%total {} (fluidty-uniq _ _ _).
tm : type.
tm/lam : ty -> (tm -> tm) -> tm.
tm/app : tm -> tm -> tm.
tm/z : tm.
tm/s : tm -> tm.
tm/if : tm -> tm -> (tm -> tm) -> tm.
tm/fix : ty -> (tm -> tm) -> tm.
tm/access : fluid -> tm.
tm/fluid-let : fluid -> tm -> tm -> tm.
tm/susp : tm -> tm.
tm/unsusp : tm -> tm.
tm/let : tm -> ty -> (tm -> tm) -> tm
   = [e:tm] [t:ty] [f:tm -> tm] tm/app (tm/lam t ([x:tm] f x)) e.
eqtm : tm -> tm -> type.
eqtm/refl : {E:tm} eqtm E E.
v : tm -> type.
v/lam : {T:ty} {E:tm -> tm} v (tm/lam T ([x:tm] E x)).
v/z : v tm/z.
v/s : {E:tm} v E -> v (tm/s E).
v/susp : {E:tm} v (tm/susp E).
frame : type.
-- : type.
--- : --.
f/app1 : -- -> tm -> frame.
f/app2 : {t:tm} v t -> -- -> frame.
f/s : -- -> frame.
f/if : -- -> tm -> (tm -> tm) -> frame.
f/fluid-let : fluid -> -- -> tm -> frame.
f/fluid-bind : fluid -> ({t:tm} v t -> frame).
f/unsusp : -- -> frame.
stack : type.
emp : stack.
; : frame -> stack -> stack.
%infix right 10 ;.
state : type.
>> : stack -> tm -> state.
<< : stack -> ({t:tm} v t -> state).
of : tm -> ty -> fluids -> type.
of/weaken :
   {E:tm} {T:ty} {Bs:fluids} {Cs:fluids} of E T Bs -> subset Bs Cs -> of E T Cs.
of/lam :
   {T:ty} {E:tm -> tm} {T':ty}
      ({x:tm} of x T # -> of (E x) T' #)
         -> of (tm/lam T ([x:tm] E x)) (ty/arrow T T') #.
of/app :
   {E1:tm} {T:ty} {T':ty} {Bs:fluids} {E2:tm}
      of E1 (ty/arrow T T') Bs -> of E2 T Bs -> of (tm/app E1 E2) T' Bs.
of/z : of tm/z ty/nat #.
of/s : {E:tm} {Bs:fluids} of E ty/nat Bs -> of (tm/s E) ty/nat Bs.
of/if :
   {E:tm} {Bs:fluids} {E1:tm} {T:ty} {E2:tm -> tm}
      of E ty/nat Bs -> of E1 T Bs -> ({x:tm} of x ty/nat # -> of (E2 x) T Bs)
         -> of (tm/if E E1 ([x:tm] E2 x)) T Bs.
of/fix :
   {T:ty} {E:tm -> tm}
      ({x:tm} of x T # -> of (E x) T #) -> of (tm/fix T ([x:tm] E x)) T #.
of/access : {A:fluid} {T:ty} fluidty A T -> of (tm/access A) T (A , #).
of/fluid-let :
   {A:fluid} {Tf:ty} {E1:tm} {Bs:fluids} {E2:tm} {T:ty}
      fluidty A Tf -> of E1 Tf Bs -> of E2 T (A , Bs)
         -> of (tm/fluid-let A E1 E2) T Bs.
of/susp :
   {E:tm} {T:ty} {Bs:fluids} of E T Bs -> of (tm/susp E) (ty/mayuse T Bs) #.
of/unsusp :
   {As:fluids} {Bs:fluids} {Cs:fluids} {E:tm} {T:ty}
      merge As Bs Cs -> of E (ty/mayuse T As) Bs -> of (tm/unsusp E) T Cs.
offrame : frame -> ty -> fluids -> ty -> fluids -> type.
offrame/app1 :
   {E2:tm} {T':ty} {Bs:fluids} {T:ty}
      of E2 T' Bs -> offrame (f/app1 --- E2) (ty/arrow T' T) Bs T Bs.
offrame/app2 :
   {E1:tm} {T':ty} {T:ty} {V:v E1} {Bs:fluids}
      of E1 (ty/arrow T' T) # -> offrame (f/app2 E1 V ---) T' Bs T Bs.
offrame/s : {Bs:fluids} offrame (f/s ---) ty/nat Bs ty/nat Bs.
offrame/if :
   {E1:tm} {T:ty} {Bs:fluids} {E2:tm -> tm}
      of E1 T Bs -> ({x:tm} of x ty/nat # -> of (E2 x) T Bs)
         -> offrame (f/if --- E1 ([x:tm] E2 x)) ty/nat Bs T Bs.
offrame/fluid-let :
   {A:fluid} {T:ty} {E:tm} {T':ty} {Bs:fluids}
      fluidty A T -> of E T' (A , Bs)
         -> offrame (f/fluid-let A --- E) T Bs T' Bs.
offrame/fluid-bind :
   {A:fluid} {Tf:ty} {E:tm} {Dv:v E} {T:ty} {Bs:fluids}
      fluidty A Tf -> of E Tf # -> offrame (f/fluid-bind A E Dv) T (A , Bs) T Bs.
offrame/unsusp :
   {As:fluids} {Bs:fluids} {Cs:fluids} {T:ty}
      merge As Bs Cs -> offrame (f/unsusp ---) (ty/mayuse T As) Bs T Cs.
ofstack : stack -> ty -> fluids -> type.
ofstack/weaken :
   {K:stack} {T:ty} {Cs:fluids} {Bs:fluids}
      ofstack K T Cs -> subset Bs Cs -> ofstack K T Bs.
ofstack/emp : {T:ty} ofstack emp T #.
ofstack/frame :
   {F:frame} {Bs:ty} {T:fluids} {Bs':ty} {Cs':fluids} {K:stack}
      offrame F Bs T Bs' Cs' -> ofstack K Bs' Cs' -> ofstack (F ; K) Bs T.
ok : state -> type.
ok>> :
   {K:stack} {T:ty} {Bs:fluids} {E:tm}
      ofstack K T Bs -> of E T Bs -> ok (>> K E).
ok<< :
   {K:stack} {T:ty} {Bs:fluids} {E:tm}
      ofstack K T Bs -> of E T Bs -> ({V:v E} ok (<< K E V)).
lookup : fluid -> stack -> ({t:tm} v t -> type).
lookup/app1 :
   {F:fluid} {K:stack} {Val:tm} {Dv:v Val} {E2:tm}
      lookup F K Val Dv -> lookup F (f/app1 --- E2 ; K) Val Dv.
lookup/app2 :
   {F:fluid} {K:stack} {Val:tm} {Dv:v Val} {E1:tm} {DV:v E1}
      lookup F K Val Dv -> lookup F (f/app2 E1 DV --- ; K) Val Dv.
lookup/s :
   {F:fluid} {K:stack} {Val:tm} {Dv:v Val}
      lookup F K Val Dv -> lookup F (f/s --- ; K) Val Dv.
lookup/if :
   {F:fluid} {K:stack} {Val:tm} {Dv:v Val} {E1:tm} {E2:tm -> tm}
      lookup F K Val Dv -> lookup F (f/if --- E1 ([x:tm] E2 x) ; K) Val Dv.
lookup/flet :
   {F:fluid} {K:stack} {Val:tm} {Dv:v Val} {A:fluid} {E2:tm}
      lookup F K Val Dv -> lookup F (f/fluid-let A --- E2 ; K) Val Dv.
lookup/ususp :
   {F:fluid} {K:stack} {Val:tm} {Dv:v Val}
      lookup F K Val Dv -> lookup F (f/unsusp --- ; K) Val Dv.
lookup/hit :
   {A:fluid} {B:fluid} {Val:tm} {Dv:v Val} {K:stack}
      eqfluid A B -> lookup A (f/fluid-bind B Val Dv ; K) Val Dv.
lookup/miss :
   {A:fluid} {B:fluid} {K:stack} {Val:tm} {Dv:v Val} {X1:tm} {X2:v X1}
      neqfluid A B -> lookup A K Val Dv
         -> lookup A (f/fluid-bind B X1 X2 ; K) Val Dv.
step : state -> state -> type.
step/lam :
   {K:stack} {T:ty} {E:tm -> tm}
      step (>> K (tm/lam T ([x:tm] E x))) (<< K (tm/lam T ([x:tm] E x)) v/lam).
step/app1 :
   {K:stack} {E1:tm} {E2:tm}
      step (>> K (tm/app E1 E2)) (>> (f/app1 --- E2 ; K) E1).
step/app2 :
   {E2:tm} {K:stack} {V:tm} {DV:v V}
      step (<< (f/app1 --- E2 ; K) V DV) (>> (f/app2 V DV --- ; K) E2).
step/appr :
   {T:ty} {E:tm -> tm} {DV:v (tm/lam T ([x:tm] E x))} {K:stack} {V:tm} {X1:v V}
      step (<< (f/app2 (tm/lam T ([x:tm] E x)) DV --- ; K) V X1) (>> K (E V)).
step/z : {K:stack} step (>> K tm/z) (<< K tm/z v/z).
step/s : {K:stack} {E:tm} step (>> K (tm/s E)) (>> (f/s --- ; K) E).
step/sr :
   {K:stack} {V:tm} {DV:v V}
      step (<< (f/s --- ; K) V DV) (<< K (tm/s V) (v/s DV)).
step/if :
   {K:stack} {E:tm} {E1:tm} {E2:tm -> tm}
      step (>> K (tm/if E E1 ([x:tm] E2 x)))
         (>> (f/if --- E1 ([x:tm] E2 x) ; K) E).
step/ifz :
   {E1:tm} {E2:tm -> tm} {K:stack} {X1:v tm/z}
      step (<< (f/if --- E1 ([x:tm] E2 x) ; K) tm/z X1) (>> K E1).
step/ifs :
   {E1:tm} {E2:tm -> tm} {K:stack} {E:tm} {X1:v (tm/s E)}
      step (<< (f/if --- E1 ([x:tm] E2 x) ; K) (tm/s E) X1) (>> K (E2 E)).
step/fix :
   {K:stack} {T:ty} {E:tm -> tm}
      step (>> K (tm/fix T ([x:tm] E x))) (>> K (E (tm/fix T ([x:tm] E x)))).
step/access :
   {A:fluid} {K:stack} {V:tm} {Dv:v V}
      lookup A K V Dv -> step (>> K (tm/access A)) (<< K V Dv).
step/flet1 :
   {K:stack} {A:fluid} {E1:tm} {E2:tm}
      step (>> K (tm/fluid-let A E1 E2)) (>> (f/fluid-let A --- E2 ; K) E1).
step/flet2 :
   {A:fluid} {E2:tm} {K:stack} {V:tm} {DV:v V}
      step (<< (f/fluid-let A --- E2 ; K) V DV)
         (>> (f/fluid-bind A V DV ; K) E2).
step/fletr :
   {A:fluid} {Vbound:tm} {DVbound:v Vbound} {K:stack} {V:tm} {DV:v V}
      step (<< (f/fluid-bind A Vbound DVbound ; K) V DV) (<< K V DV).
step/susp : {K:stack} {E:tm} step (>> K (tm/susp E)) (<< K (tm/susp E) v/susp).
step/ususp :
   {K:stack} {E:tm} step (>> K (tm/unsusp E)) (>> (f/unsusp --- ; K) E).
step/ususpr :
   {K:stack} {E:tm} {X1:v (tm/susp E)}
      step (<< (f/unsusp --- ; K) (tm/susp E) X1) (>> K E).
nstuck : state -> type.
nstuck/step : {E:state} {E':state} step E E' -> nstuck E.
nstuck/final : {V:tm} {DV:v V} nstuck (<< emp V DV).
access-stack :
   {A:fluid} {Bs:fluids} {K:stack} {T:ty} {E:tm} {Dv:v E} {Tf:ty}
      in A Bs -> ofstack K T Bs -> lookup A K E Dv -> fluidty A Tf -> of E Tf #
         -> type.
%mode +{A:fluid} +{Bs:fluids} +{K:stack} +{T:ty} -{E:tm} -{Dv:v E} -{Tf:ty}
   +{A1:in A Bs} +{B:ofstack K T Bs} -{C:lookup A K E Dv} -{D:fluidty A Tf}
   -{E1:of E Tf #} (access-stack A1 B C D E1).
read-stack :
   {A:fluid} {B:fluid} {Cs:fluids} {E:tm} {Dv:v E} {T:ty} {K:stack} {Ev:tm}
      {Dval:v Ev} {Tf:ty}
      eq-or-in A B Cs -> decidable-fluid A B
         -> offrame (f/fluid-bind B E Dv) T (B , Cs) T Cs -> ofstack K T Cs
         -> lookup A (f/fluid-bind B E Dv ; K) Ev Dval -> fluidty A Tf
         -> of Ev Tf # -> type.
%mode +{A:fluid} +{B:fluid} +{Cs:fluids} +{E:tm} +{Dv:v E} +{T:ty} +{K:stack} -{Ev:tm}
   -{Dval:v Ev} -{Tf:ty} +{A1:eq-or-in A B Cs} +{G:decidable-fluid A B}
   +{B1:offrame (f/fluid-bind B E Dv) T (B , Cs) T Cs} +{C:ofstack K T Cs}
   -{D:lookup A (f/fluid-bind B E Dv ; K) Ev Dval} -{E1:fluidty A Tf}
   -{F:of Ev Tf #} (read-stack A1 G B1 C D E1 F).
- :
   {B:fluid} {X1:fluids} {E:tm} {X2:v E} {X3:ty} {X4:stack} {Tf:ty}
      {X5:decidable-fluid B B} {Dfluid:fluidty B Tf} {Dval:of E Tf #}
      {X6:ofstack X4 X3 X1}
      read-stack eq-or-in/eq X5 (offrame/fluid-bind Dfluid Dval) X6
         (lookup/hit eqfluid/refl) Dfluid Dval.
- :
   {B:fluid} {X1:fluids} {E:tm} {X2:v E} {X3:ty} {X4:stack} {Tf:ty}
      {X5:eq-or-in B B X1} {Dfluid:fluidty B Tf} {Dval:of E Tf #}
      {X6:ofstack X4 X3 X1}
      read-stack X5 decidable-fluid/eq (offrame/fluid-bind Dfluid Dval) X6
         (lookup/hit eqfluid/refl) Dfluid Dval.
- :
   {X1:fluid} {X2:fluids} {X3:stack} {X4:ty} {X5:tm} {X6:v X5} {X7:ty}
      {In:in X1 X2} {Dstack:ofstack X3 X4 X2} {Look:lookup X1 X3 X5 X6}
      {Dfluid:fluidty X1 X7} {Dval:of X5 X7 #} {X8:fluid} {X9:tm} {X10:v X9}
      {Neq:neqfluid X1 X8}
      {X11:offrame (f/fluid-bind X8 X9 X10) X4 (X8 , X2) X4 X2}
      access-stack In Dstack Look Dfluid Dval
         -> read-stack (eq-or-in/in In) (decidable-fluid/neq Neq) X11 Dstack
               (lookup/miss Neq Look) Dfluid Dval.
- :
   {A:fluid} {Cs:fluids} {X1:stack} {X2:ty} {X3:tm} {X4:v X3} {X5:ty}
      {In':in A Cs} {Dt:ofstack X1 X2 Cs} {Lookup:lookup A X1 X3 X4}
      {Df:fluidty A X5} {Dvt:of X3 X5 #} {Bs:fluids} {In:in A Bs}
      {Sub:subset Bs Cs}
      access-stack In' Dt Lookup Df Dvt -> in-subset In Sub In'
         -> access-stack In (ofstack/weaken Dt Sub) Lookup Df Dvt.
- :
   {X1:fluid} {X2:fluids} {X3:stack} {X4:ty} {X5:tm} {X6:v X5} {X7:ty}
      {In:in X1 X2} {Dt:ofstack X3 X4 X2} {Look:lookup X1 X3 X5 X6}
      {Df:fluidty X1 X7} {Dvt:of X5 X7 #} {X8:tm} {X9:ty} {X10:of X8 X9 X2}
      access-stack In Dt Look Df Dvt
         -> access-stack In (ofstack/frame (offrame/app1 X10) Dt)
               (lookup/app1 Look) Df Dvt.
- :
   {X1:fluid} {X2:fluids} {X3:stack} {X4:ty} {X5:tm} {X6:v X5} {X7:ty}
      {In:in X1 X2} {Dt:ofstack X3 X4 X2} {Look:lookup X1 X3 X5 X6}
      {Df:fluidty X1 X7} {Dvt:of X5 X7 #} {X8:tm} {X9:v X8} {X10:ty}
      {X11:of X8 (ty/arrow X10 X4) #}
      access-stack In Dt Look Df Dvt
         -> access-stack In (ofstack/frame (offrame/app2 X11) Dt)
               (lookup/app2 Look) Df Dvt.
- :
   {X1:fluid} {X2:fluids} {X3:stack} {X4:tm} {X5:v X4} {X6:ty} {In:in X1 X2}
      {Dt:ofstack X3 ty/nat X2} {Look:lookup X1 X3 X4 X5} {Df:fluidty X1 X6}
      {Dvt:of X4 X6 #}
      access-stack In Dt Look Df Dvt
         -> access-stack In (ofstack/frame offrame/s Dt) (lookup/s Look) Df Dvt.
- :
   {X1:fluid} {X2:fluids} {X3:stack} {X4:ty} {X5:tm} {X6:v X5} {X7:ty}
      {In:in X1 X2} {Dt:ofstack X3 X4 X2} {Look:lookup X1 X3 X5 X6}
      {Df:fluidty X1 X7} {Dvt:of X5 X7 #} {X8:tm} {X9:tm -> tm}
      {X10:of X8 X4 X2} {X11:{x:tm} of x ty/nat # -> of (X9 x) X4 X2}
      access-stack In Dt Look Df Dvt
         -> access-stack In
               (ofstack/frame
                   (offrame/if X10 ([x:tm] [x1:of x ty/nat #] X11 x x1)) Dt)
               (lookup/if Look) Df Dvt.
- :
   {X1:fluid} {X2:fluids} {X3:stack} {X4:ty} {X5:tm} {X6:v X5} {X7:ty}
      {In:in X1 X2} {Dt:ofstack X3 X4 X2} {Look:lookup X1 X3 X5 X6}
      {Df:fluidty X1 X7} {Dvt:of X5 X7 #} {X8:fluid} {X9:tm} {X10:ty}
      {X11:fluidty X8 X10} {X12:of X9 X4 (X8 , X2)}
      access-stack In Dt Look Df Dvt
         -> access-stack In (ofstack/frame (offrame/fluid-let X11 X12) Dt)
               (lookup/flet Look) Df Dvt.
- :
   {A:fluid} {B:fluid} {Cs:fluids} {X1:tm} {X2:v X1} {X3:ty} {X4:stack} {E:tm}
      {X5:v E} {Tf:ty} {Deq-or-in:eq-or-in A B Cs}
      {Deq-or-neq:decidable-fluid A B}
      {Dframe:offrame (f/fluid-bind B X1 X2) X3 (B , Cs) X3 Cs}
      {Dstack:ofstack X4 X3 Cs} {Look:lookup A (f/fluid-bind B X1 X2 ; X4) E X5}
      {Df:fluidty A Tf} {Dvt:of E Tf #} {In:in A (B , Cs)}
      read-stack Deq-or-in Deq-or-neq Dframe Dstack Look Df Dvt
         -> eq-or-neq-total A B Deq-or-neq -> in-inversion In Deq-or-in
         -> access-stack In (ofstack/frame Dframe Dstack) Look Df Dvt.
- :
   {X1:fluid} {Cs:fluids} {K:stack} {T:ty} {X2:tm} {X3:v X2} {X4:ty}
      {In':in X1 Cs} {Dt:ofstack K T Cs} {Look:lookup X1 K X2 X3}
      {Df:fluidty X1 X4} {Dvt:of X2 X4 #} {Bs:fluids} {As:fluids} {In:in X1 Bs}
      {Merge:merge As Bs Cs}
      access-stack In' Dt Look Df Dvt -> in-merge2 In Merge In'
         -> access-stack In (ofstack/frame (offrame/unsusp Merge) Dt)
               (lookup/ususp Look) Df Dvt.
%worlds () (access-stack _ _ _ _ _) (read-stack _ _ _ _ _ _ _).
%total (T S) (access-stack _ T _ _ _) (read-stack _ _ _ S _ _ _).
canon-arrow :
   {E1:tm} {T1:ty} {T2:ty} {Bs:fluids} {E:tm -> tm}
      of E1 (ty/arrow T1 T2) Bs -> v E1 -> eqtm E1 (tm/lam T1 ([x:tm] E x))
         -> type.
- :
   {X1:tm} {X2:ty} {X3:ty} {X4:fluids} {X5:tm -> tm}
      {T:of X1 (ty/arrow X2 X3) X4} {Dv:v X1}
      {Eq:eqtm X1 (tm/lam X2 ([x:tm] X5 x))} {X6:fluids} {X7:subset X4 X6}
      canon-arrow T Dv Eq -> canon-arrow (of/weaken T X7) Dv Eq.
- :
   {X1:ty} {X2:tm -> tm} {X3:ty} {X4:{x:tm} of x X1 # -> of (X2 x) X3 #}
      canon-arrow (of/lam ([x:tm] [x1:of x X1 #] X4 x x1)) v/lam eqtm/refl.
%mode +{E1:tm} +{T1:ty} +{T2:ty} +{Bs:fluids} -{E:tm -> tm}
   +{A:of E1 (ty/arrow T1 T2) Bs} +{B:v E1}
   -{C:eqtm E1 (tm/lam T1 ([x:tm] E x))} (canon-arrow A B C).
%worlds () (canon-arrow _ _ _).
%total T (canon-arrow T _ _).
z-or-s : tm -> type.
z-or-s/z : z-or-s tm/z.
z-or-s/s : {E:tm} z-or-s (tm/s E).
canon-nat : {E1:tm} {Bs:fluids} of E1 ty/nat Bs -> v E1 -> z-or-s E1 -> type.
- :
   {X1:tm} {X2:fluids} {T:of X1 ty/nat X2} {Dv:v X1} {Eq:z-or-s X1} {X3:fluids}
      {X4:subset X2 X3} canon-nat T Dv Eq -> canon-nat (of/weaken T X4) Dv Eq.
- : canon-nat of/z v/z z-or-s/z.
- :
   {X1:tm} {X2:fluids} {X3:of X1 ty/nat X2} {X4:v X1}
      canon-nat (of/s X3) (v/s X4) z-or-s/s.
%mode +{E1:tm} +{Bs:fluids} +{A:of E1 ty/nat Bs} +{B:v E1} -{C:z-or-s E1}
   (canon-nat A B C).
%worlds () (canon-nat _ _ _).
%total T (canon-nat T _ _).
canon-mayuse :
   {E1:tm} {T:ty} {As:fluids} {Bs:fluids} {E:tm}
      of E1 (ty/mayuse T As) Bs -> v E1 -> eqtm E1 (tm/susp E) -> type.
- :
   {X1:tm} {X2:ty} {X3:fluids} {X4:fluids} {X5:tm}
      {T:of X1 (ty/mayuse X2 X3) X4} {Dv:v X1} {Eq:eqtm X1 (tm/susp X5)}
      {X6:fluids} {X7:subset X4 X6}
      canon-mayuse T Dv Eq -> canon-mayuse (of/weaken T X7) Dv Eq.
- :
   {X1:tm} {X2:ty} {X3:fluids} {X4:of X1 X2 X3}
      canon-mayuse (of/susp X4) v/susp eqtm/refl.
%mode +{E1:tm} +{T:ty} +{As:fluids} +{Bs:fluids} -{E:tm}
   +{A:of E1 (ty/mayuse T As) Bs} +{B:v E1} -{C:eqtm E1 (tm/susp E)}
   (canon-mayuse A B C).
%worlds () (canon-mayuse _ _ _).
%total T (canon-mayuse T _ _).
progress>> :
   {K:stack} {T:ty} {Bs:fluids} {E:tm} {S':state}
      ofstack K T Bs -> of E T Bs -> step (>> K E) S' -> type.
- :
   {X1:stack} {X2:ty} {X3:fluids} {X4:tm} {X5:state} {X6:fluids}
      {TK:ofstack X1 X2 X6} {Sub:subset X3 X6} {TE:of X4 X2 X3}
      {Step:step (>> X1 X4) X5}
      progress>> (ofstack/weaken TK Sub) TE Step
         -> progress>> TK (of/weaken TE Sub) Step.
- :
   {X1:stack} {X2:ty} {X3:ty} {X4:tm -> tm} {TK:ofstack X1 (ty/arrow X2 X3) #}
      {X5:{x:tm} of x X2 # -> of (X4 x) X3 #}
      progress>> TK (of/lam ([x:tm] [x1:of x X2 #] X5 x x1)) step/lam.
- :
   {X1:stack} {X2:ty} {X3:fluids} {X4:tm} {X5:tm} {TK:ofstack X1 X2 X3} {X6:ty}
      {X7:of X4 (ty/arrow X6 X2) X3} {X8:of X5 X6 X3}
      progress>> TK (of/app X7 X8) step/app1.
- : {X1:stack} {TK:ofstack X1 ty/nat #} progress>> TK of/z step/z.
- :
   {X1:stack} {X2:fluids} {X3:tm} {TK:ofstack X1 ty/nat X2} {X4:of X3 ty/nat X2}
      progress>> TK (of/s X4) step/s.
- :
   {X1:stack} {X2:ty} {X3:fluids} {X4:tm} {X5:tm} {X6:tm -> tm}
      {TK:ofstack X1 X2 X3} {X7:of X4 ty/nat X3} {X8:of X5 X2 X3}
      {X9:{x:tm} of x ty/nat # -> of (X6 x) X2 X3}
      progress>> TK (of/if X7 X8 ([x:tm] [x1:of x ty/nat #] X9 x x1)) step/if.
- :
   {X1:stack} {X2:ty} {X3:tm -> tm} {TK:ofstack X1 X2 #}
      {X4:{x:tm} of x X2 # -> of (X3 x) X2 #}
      progress>> TK (of/fix ([x:tm] [x1:of x X2 #] X4 x x1)) step/fix.
- :
   {A:fluid} {X1:stack} {T:ty} {X2:tm} {X3:v X2} {X4:ty}
      {TK:ofstack X1 T (A , #)} {Look:lookup A X1 X2 X3} {X5:fluidty A X4}
      {X6:of X2 X4 #} {TA:fluidty A T}
      access-stack in/z TK Look X5 X6
         -> progress>> TK (of/access TA) (step/access Look).
- :
   {X1:stack} {X2:ty} {X3:fluids} {X4:fluid} {X5:tm} {X6:tm}
      {TK:ofstack X1 X2 X3} {X7:ty} {X8:fluidty X4 X7} {X9:of X5 X7 X3}
      {X10:of X6 X2 (X4 , X3)} progress>> TK (of/fluid-let X8 X9 X10) 
step/flet1.
- :
   {X1:stack} {X2:ty} {X3:fluids} {X4:tm} {TK:ofstack X1 (ty/mayuse X2 X3) #}
      {X5:of X4 X2 X3} progress>> TK (of/susp X5) step/susp.
- :
   {X1:stack} {X2:ty} {X3:fluids} {X4:tm} {TK:ofstack X1 X2 X3} {X5:fluids}
      {X6:fluids} {X7:merge X5 X6 X3} {X8:of X4 (ty/mayuse X2 X5) X6}
      progress>> TK (of/unsusp X7 X8) step/ususp.
%mode +{K:stack} +{T:ty} +{Bs:fluids} +{E:tm} -{S':state} +{A:ofstack K T Bs}
   +{B:of E T Bs} -{C:step (>> K E) S'} (progress>> A B C).
%worlds () (progress>> _ _ _).
%total T (progress>> _ T _).
progress<< :
   {K:stack} {T:ty} {Bs:fluids} {E:tm}
      ofstack K T Bs -> of E T Bs -> ({Dv:v E} nstuck (<< K E Dv) -> type).
%mode +{K:stack} +{T:ty} +{Bs:fluids} +{E:tm} +{A:ofstack K T Bs} +{B:of E T Bs}
   +{C:v E} -{D:nstuck (<< K E C)} (progress<< A B C D).
- :
   {X1:stack} {X2:ty} {X3:fluids} {X4:tm} {TK:ofstack X1 X2 X3} {X5:fluids}
      {TE:of X4 X2 X5} {Sub:subset X5 X3} {Dv:v X4} {NS:nstuck (<< X1 X4 Dv)}
      progress<< TK (of/weaken TE Sub) Dv NS
         -> progress<< (ofstack/weaken TK Sub) TE Dv NS.
- :
   {X1:ty} {X2:tm} {TE:of X2 X1 #} {Dv:v X2}
      progress<< ofstack/emp TE Dv nstuck/final.
- :
   {X1:tm} {X2:stack} {X3:ty} {X4:ty} {X5:fluids} {X6:tm} {TE2:of X1 X3 X5}
      {TK:ofstack X2 X4 X5} {TE1:of X6 (ty/arrow X3 X4) X5} {Dv:v X6}
      progress<< (ofstack/frame (offrame/app1 TE2) TK) TE1 Dv
         (nstuck/step step/app2).
p1 :
   {E1:tm} {T1:ty} {E:tm -> tm} {S':state}
      eqtm E1 (tm/lam T1 ([x:tm] E x))
         -> ({Dv:v E1} {K:stack} {E2:tm} {Dv':v E2}
                step (<< (f/app2 E1 Dv --- ; K) E2 Dv') S' -> type).
- :
   {X1:ty} {X2:tm -> tm} {X3:ty} {X4:tm -> tm} {X5:stack} {X6:tm}
      {X7:eqtm (tm/lam X1 ([x:tm] X2 x)) (tm/lam X3 ([x:tm] X4 x))}
      {X8:v (tm/lam X1 ([x:tm] X2 x))} {X9:v X6} p1 X7 X8 X5 X6 X9 step/appr.
%mode +{E1:tm} +{T1:ty} +{E:tm -> tm} -{S':state}
   +{A:eqtm E1 (tm/lam T1 ([x:tm] E x))} +{B:v E1} +{C:stack} +{D:tm} +{E2:v D}
   -{F:step (<< (f/app2 E1 B --- ; C) D E2) S'} (p1 A B C D E2 F).
%worlds () (p1 _ _ _ _ _ _).
%total {} (p1 _ _ _ _ _ _).
- :
   {E1:tm} {T':ty} {X1:tm -> tm} {X2:state}
      {Eq:eqtm E1 (tm/lam T' ([x:tm] X1 x))} {Dv:v E1} {X3:stack} {X4:tm}
      {X5:v X4} {Step:step (<< (f/app2 E1 Dv --- ; X3) X4 X5) X2} {T:ty}
      {TE1:of E1 (ty/arrow T' T) #} {Bs:fluids} {TK:ofstack X3 T Bs}
      {TE2:of X4 T' Bs}
      p1 Eq Dv X3 X4 X5 Step -> canon-arrow TE1 Dv Eq
         -> progress<< (ofstack/frame (offrame/app2 TE1) TK) TE2 X5
               (nstuck/step Step).
- :
   {X1:stack} {X2:fluids} {X3:tm} {TK:ofstack X1 ty/nat X2}
      {TE1:of X3 ty/nat X2} {Dv:v X3}
      progress<< (ofstack/frame offrame/s TK) TE1 Dv (nstuck/step step/sr).
p2 :
   {E:tm} {S':state}
      z-or-s E
         -> ({E1:tm} {E2:tm -> tm} {K:stack} {Dv:v E}
                step (<< (f/if --- E1 ([x:tm] E2 x) ; K) E Dv) S' -> type).
- :
   {X1:stack} {X2:tm} {X3:tm -> tm} {X4:v tm/z}
      p2 z-or-s/z X2 ([x:tm] X3 x) X1 X4 step/ifz.
- :
   {X1:tm} {X2:stack} {X3:tm -> tm} {X4:tm} {X5:v (tm/s X1)}
      p2 z-or-s/s X4 ([x:tm] X3 x) X2 X5 step/ifs.
%mode +{E:tm} -{S':state} +{A:z-or-s E} +{B:tm} +{C:tm -> tm} +{D:stack} +{F:v E}
   -{E1:step (<< (f/if --- B ([x:tm] C x) ; D) E F) S'} (p2 A B C D F E1).
%worlds () (p2 _ _ _ _ _ _).
%total {} (p2 _ _ _ _ _ _).
- :
   {X1:tm} {X2:state} {Eq:z-or-s X1} {X3:tm} {X4:tm -> tm} {X5:stack} {Dv:v X1}
      {Step:step (<< (f/if --- X3 ([x:tm] X4 x) ; X5) X1 Dv) X2} {X6:fluids}
      {TE:of X1 ty/nat X6} {X7:ty} {X8:of X3 X7 X6}
      {X9:{x:tm} of x ty/nat # -> of (X4 x) X7 X6} {TK:ofstack X5 X7 X6}
      p2 Eq X3 ([x:tm] X4 x) X5 Dv Step -> canon-nat TE Dv Eq
         -> progress<<
               (ofstack/frame
                   (offrame/if X8 ([x:tm] [x1:of x ty/nat #] X9 x x1)) TK) TE Dv
               (nstuck/step Step).
- :
   {X1:fluid} {X2:tm} {X3:stack} {X4:ty} {X5:fluids} {X6:tm} {X7:ty}
      {X8:fluidty X1 X4} {X9:of X2 X7 (X1 , X5)} {TK:ofstack X3 X7 X5}
      {TE:of X6 X4 X5} {Dv:v X6}
      progress<< (ofstack/frame (offrame/fluid-let X8 X9) TK) TE Dv
         (nstuck/step step/flet2).
- :
   {X1:fluid} {X2:tm} {X3:v X2} {X4:stack} {X5:ty} {X6:fluids} {X7:tm} {X8:ty}
      {X9:fluidty X1 X8} {X10:of X2 X8 #} {TK:ofstack X4 X5 X6}
      {TE:of X7 X5 (X1 , X6)} {Dv:v X7}
      progress<< (ofstack/frame (offrame/fluid-bind X9 X10) TK) TE Dv
         (nstuck/step step/fletr).
p3 :
   {E:tm} {E':tm} {S':state}
      eqtm E (tm/susp E')
         -> ({K:stack} {Dv:v E} step (<< (f/unsusp --- ; K) E Dv) S' -> type).
- : {X1:tm} {X2:stack} {X3:v (tm/susp X1)} p3 eqtm/refl X2 X3 step/ususpr.
%mode +{E:tm} +{E':tm} -{S':state} +{A:eqtm E (tm/susp E')} +{B:stack} +{D:v E}
   -{C:step (<< (f/unsusp --- ; B) E D) S'} (p3 A B D C).
%worlds () (p3 _ _ _ _).
%total {} (p3 _ _ _ _).
- :
   {X1:tm} {X2:tm} {X3:state} {Eq:eqtm X1 (tm/susp X2)} {X4:stack} {Dv:v X1}
      {Step:step (<< (f/unsusp --- ; X4) X1 Dv) X3} {X5:ty} {X6:fluids}
      {X7:fluids} {TE:of X1 (ty/mayuse X5 X6) X7} {X8:fluids}
      {X9:merge X6 X7 X8} {TK:ofstack X4 X5 X8}
      p3 Eq X4 Dv Step -> canon-mayuse TE Dv Eq
         -> progress<< (ofstack/frame (offrame/unsusp X9) TK) TE Dv
               (nstuck/step Step).
%worlds () (progress<< _ _ _ _).
%total T (progress<< T _ _ _).
progress : {S:state} ok S -> nstuck S -> type.
- :
   {X1:stack} {X2:ty} {X3:fluids} {X4:tm} {X5:state} {TK:ofstack X1 X2 X3}
      {TE:of X4 X2 X3} {Step:step (>> X1 X4) X5}
      progress>> TK TE Step -> progress (ok>> TK TE) (nstuck/step Step).
- :
   {X1:stack} {X2:ty} {X3:fluids} {X4:tm} {TK:ofstack X1 X2 X3} {TE:of X4 X2 X3}
      {Dv:v X4} {NS:nstuck (<< X1 X4 Dv)}
      progress<< TK TE Dv NS -> progress (ok<< TK TE Dv) NS.
%mode +{S:state} +{A:ok S} -{B:nstuck S} (progress A B).
%worlds () (progress _ _).
%total {} (progress _ _).
access-stack' :
   {A:fluid} {Bs:fluids} {K:stack} {T:ty} {E:tm} {Dv:v E} {Tf:ty}
      in A Bs -> ofstack K T Bs -> lookup A K E Dv -> fluidty A Tf -> of E Tf #
         -> type.
%mode +{A:fluid} +{Bs:fluids} +{K:stack} +{T:ty} +{E:tm} +{Dv:v E} -{Tf:ty}
   +{A1:in A Bs} +{B:ofstack K T Bs} +{C:lookup A K E Dv} -{D:fluidty A Tf}
   -{E1:of E Tf #} (access-stack' A1 B C D E1).
read-stack' :
   {A:fluid} {B:fluid} {Cs:fluids} {E:tm} {Dv:v E} {T:ty} {K:stack} {Ev:tm}
      {Dval:v Ev} {Tf:ty}
      eq-or-in A B Cs -> decidable-fluid A B
         -> offrame (f/fluid-bind B E Dv) T (B , Cs) T Cs -> ofstack K T Cs
         -> lookup A (f/fluid-bind B E Dv ; K) Ev Dval -> fluidty A Tf
         -> of Ev Tf # -> type.
%mode +{A:fluid} +{B:fluid} +{Cs:fluids} +{E:tm} +{Dv:v E} +{T:ty} +{K:stack} +{Ev:tm}
   +{Dval:v Ev} -{Tf:ty} +{A1:eq-or-in A B Cs} +{G:decidable-fluid A B}
   +{B1:offrame (f/fluid-bind B E Dv) T (B , Cs) T Cs} +{C:ofstack K T Cs}
   +{D:lookup A (f/fluid-bind B E Dv ; K) Ev Dval} -{E1:fluidty A Tf}
   -{F:of Ev Tf #} (read-stack' A1 G B1 C D E1 F).
- :
   {B:fluid} {X1:fluids} {E:tm} {X2:v E} {X3:ty} {X4:stack} {Tf:ty}
      {X5:decidable-fluid B B} {Dfluid:fluidty B Tf} {Dval:of E Tf #}
      {X6:ofstack X4 X3 X1}
      read-stack' eq-or-in/eq X5 (offrame/fluid-bind Dfluid Dval) X6
         (lookup/hit eqfluid/refl) Dfluid Dval.
- :
   {B:fluid} {X1:fluids} {E:tm} {X2:v E} {X3:ty} {X4:stack} {Tf:ty}
      {X5:eq-or-in B B X1} {Dfluid:fluidty B Tf} {Dval:of E Tf #}
      {X6:ofstack X4 X3 X1}
      read-stack' X5 decidable-fluid/eq (offrame/fluid-bind Dfluid Dval) X6
         (lookup/hit eqfluid/refl) Dfluid Dval.
- :
   {X1:fluid} {X2:fluids} {X3:stack} {X4:ty} {X5:tm} {X6:v X5} {X7:ty}
      {In:in X1 X2} {Dstack:ofstack X3 X4 X2} {Look:lookup X1 X3 X5 X6}
      {Dfluid:fluidty X1 X7} {Dval:of X5 X7 #} {X8:fluid} {X9:tm} {X10:v X9}
      {Neq:neqfluid X1 X8}
      {X11:offrame (f/fluid-bind X8 X9 X10) X4 (X8 , X2) X4 X2}
      access-stack' In Dstack Look Dfluid Dval
         -> read-stack' (eq-or-in/in In) (decidable-fluid/neq Neq) X11 Dstack
               (lookup/miss Neq Look) Dfluid Dval.
- :
   {A:fluid} {Cs:fluids} {X1:stack} {X2:ty} {X3:tm} {X4:v X3} {X5:ty}
      {In':in A Cs} {Dt:ofstack X1 X2 Cs} {Lookup:lookup A X1 X3 X4}
      {Df:fluidty A X5} {Dvt:of X3 X5 #} {Bs:fluids} {In:in A Bs}
      {Sub:subset Bs Cs}
      access-stack' In' Dt Lookup Df Dvt -> in-subset In Sub In'
         -> access-stack' In (ofstack/weaken Dt Sub) Lookup Df Dvt.
- :
   {X1:fluid} {X2:fluids} {X3:stack} {X4:ty} {X5:tm} {X6:v X5} {X7:ty}
      {In:in X1 X2} {Dt:ofstack X3 X4 X2} {Look:lookup X1 X3 X5 X6}
      {Df:fluidty X1 X7} {Dvt:of X5 X7 #} {X8:tm} {X9:ty} {X10:of X8 X9 X2}
      access-stack' In Dt Look Df Dvt
         -> access-stack' In (ofstack/frame (offrame/app1 X10) Dt)
               (lookup/app1 Look) Df Dvt.
- :
   {X1:fluid} {X2:fluids} {X3:stack} {X4:ty} {X5:tm} {X6:v X5} {X7:ty}
      {In:in X1 X2} {Dt:ofstack X3 X4 X2} {Look:lookup X1 X3 X5 X6}
      {Df:fluidty X1 X7} {Dvt:of X5 X7 #} {X8:tm} {X9:v X8} {X10:ty}
      {X11:of X8 (ty/arrow X10 X4) #}
      access-stack' In Dt Look Df Dvt
         -> access-stack' In (ofstack/frame (offrame/app2 X11) Dt)
               (lookup/app2 Look) Df Dvt.
- :
   {X1:fluid} {X2:fluids} {X3:stack} {X4:tm} {X5:v X4} {X6:ty} {In:in X1 X2}
      {Dt:ofstack X3 ty/nat X2} {Look:lookup X1 X3 X4 X5} {Df:fluidty X1 X6}
      {Dvt:of X4 X6 #}
      access-stack' In Dt Look Df Dvt
         -> access-stack' In (ofstack/frame offrame/s Dt) (lookup/s Look) Df Dvt.
- :
   {X1:fluid} {X2:fluids} {X3:stack} {X4:ty} {X5:tm} {X6:v X5} {X7:ty}
      {In:in X1 X2} {Dt:ofstack X3 X4 X2} {Look:lookup X1 X3 X5 X6}
      {Df:fluidty X1 X7} {Dvt:of X5 X7 #} {X8:tm} {X9:tm -> tm}
      {X10:of X8 X4 X2} {X11:{x:tm} of x ty/nat # -> of (X9 x) X4 X2}
      access-stack' In Dt Look Df Dvt
         -> access-stack' In
               (ofstack/frame
                   (offrame/if X10 ([x:tm] [x1:of x ty/nat #] X11 x x1)) Dt)
               (lookup/if Look) Df Dvt.
- :
   {X1:fluid} {X2:fluids} {X3:stack} {X4:ty} {X5:tm} {X6:v X5} {X7:ty}
      {In:in X1 X2} {Dt:ofstack X3 X4 X2} {Look:lookup X1 X3 X5 X6}
      {Df:fluidty X1 X7} {Dvt:of X5 X7 #} {X8:fluid} {X9:tm} {X10:ty}
      {X11:fluidty X8 X10} {X12:of X9 X4 (X8 , X2)}
      access-stack' In Dt Look Df Dvt
         -> access-stack' In (ofstack/frame (offrame/fluid-let X11 X12) Dt)
               (lookup/flet Look) Df Dvt.
- :
   {A:fluid} {B:fluid} {Cs:fluids} {X1:tm} {X2:v X1} {X3:ty} {X4:stack} {E:tm}
      {X5:v E} {Tf:ty} {Deq-or-in:eq-or-in A B Cs}
      {Deq-or-neq:decidable-fluid A B}
      {Dframe:offrame (f/fluid-bind B X1 X2) X3 (B , Cs) X3 Cs}
      {Dstack:ofstack X4 X3 Cs} {Look:lookup A (f/fluid-bind B X1 X2 ; X4) E X5}
      {Df:fluidty A Tf} {Dvt:of E Tf #} {In:in A (B , Cs)}
      read-stack' Deq-or-in Deq-or-neq Dframe Dstack Look Df Dvt
         -> eq-or-neq-total A B Deq-or-neq -> in-inversion In Deq-or-in
         -> access-stack' In (ofstack/frame Dframe Dstack) Look Df Dvt.
- :
   {X1:fluid} {Cs:fluids} {K:stack} {T:ty} {X2:tm} {X3:v X2} {X4:ty}
      {In':in X1 Cs} {Dt:ofstack K T Cs} {Look:lookup X1 K X2 X3}
      {Df:fluidty X1 X4} {Dvt:of X2 X4 #} {Bs:fluids} {As:fluids} {In:in X1 Bs}
      {Merge:merge As Bs Cs}
      access-stack' In' Dt Look Df Dvt -> in-merge2 In Merge In'
         -> access-stack' In (ofstack/frame (offrame/unsusp Merge) Dt)
               (lookup/ususp Look) Df Dvt.
%worlds () (access-stack' _ _ _ _ _) (read-stack' _ _ _ _ _ _ _).
%total (T S) (access-stack' _ T _ _ _) (read-stack' _ _ _ S _ _ _).
effect-value : {E:tm} {T:ty} {Bs:fluids} v E -> of E T Bs -> of E T # -> type.
- :
   {X1:tm} {X2:ty} {X3:fluids} {V:v X1} {T:of X1 X2 X3} {T':of X1 X2 #}
      {X4:fluids} {Sub:subset X3 X4}
      effect-value V T T' -> effect-value V (of/weaken T Sub) T'.
- :
   {X1:ty} {X2:tm -> tm} {X3:ty} {T:of (tm/lam X1 ([x:tm] X2 x)) X3 #}
      effect-value v/lam T T.
- : {X1:tm} {X2:ty} {T:of (tm/susp X1) X2 #} effect-value v/susp T T.
- : {X1:ty} {T:of tm/z X1 #} effect-value v/z T T.
- :
   {X1:tm} {X2:fluids} {V:v X1} {T:of X1 ty/nat X2} {T':of X1 ty/nat #}
      effect-value V T T' -> effect-value (v/s V) (of/s T) (of/s T').
%mode +{E:tm} +{T:ty} +{Bs:fluids} +{A:v E} +{B:of E T Bs} -{C:of E T #}
   (effect-value A B C).
%worlds () (effect-value _ _ _).
%total [S T] (effect-value S T _).
inv-lam :
   {T1:ty} {E:tm -> tm} {T:ty} {Bs:fluids} {T2:ty}
      of (tm/lam T1 ([x:tm] E x)) T Bs -> eqty T (ty/arrow T1 T2)
         -> ({x:tm} of x T1 # -> of (E x) T2 #) -> type.
- :
   {X1:ty} {X2:tm -> tm} {X3:ty} {X4:fluids} {X5:ty}
      {T:of (tm/lam X1 ([x:tm] X2 x)) X3 X4} {Eq:eqty X3 (ty/arrow X1 X5)}
      {Tf:{x:tm} of x X1 # -> of (X2 x) X5 #} {X6:fluids} {Sub:subset X4 X6}
      inv-lam T Eq ([x:tm] [x1:of x X1 #] Tf x x1)
         -> inv-lam (of/weaken T Sub) Eq ([x:tm] [x1:of x X1 #] Tf x x1).
- :
   {X1:ty} {X2:tm -> tm} {X3:ty} {F:{x:tm} of x X1 # -> of (X2 x) X3 #}
      inv-lam (of/lam ([x:tm] [x1:of x X1 #] F x x1)) eqty/refl
         ([x:tm] [x1:of x X1 #] F x x1).
%mode +{T1:ty} +{E:tm -> tm} +{T:ty} +{Bs:fluids} -{T2:ty}
   +{A:of (tm/lam T1 ([x:tm] E x)) T Bs} -{B:eqty T (ty/arrow T1 T2)}
   -{C:{x:tm} of x T1 # -> of (E x) T2 #} (inv-lam A B C).
%worlds () (inv-lam _ _ _).
%total T (inv-lam T _ _).
inv-app :
   {E1:tm} {E2:tm} {T:ty} {Cs:fluids} {Bs:fluids} {T':ty}
      of (tm/app E1 E2) T Cs -> subset Bs Cs -> of E1 (ty/arrow T' T) Bs
         -> of E2 T' Bs -> type.
- :
   {X1:fluids} {X2:fluids} {X3:fluids} {Sub:subset X1 X2} {Sub':subset X2 X3}
      {Sub'':subset X1 X3} {X4:tm} {X5:tm} {X6:ty} {X7:ty}
      {T:of (tm/app X4 X5) X6 X2} {T1:of X4 (ty/arrow X7 X6) X1}
      {T2:of X5 X7 X1}
      subset-trans Sub Sub' Sub'' -> inv-app T Sub T1 T2
         -> inv-app (of/weaken T Sub') Sub'' T1 T2.
- :
   {X1:fluids} {Sub:subset X1 X1} {X2:tm} {X3:tm} {X4:ty} {X5:ty}
      {T1:of X2 (ty/arrow X5 X4) X1} {T2:of X3 X5 X1}
      subset-refl X1 Sub -> inv-app (of/app T1 T2) Sub T1 T2.
%mode +{E1:tm} +{E2:tm} +{T:ty} +{Cs:fluids} -{Bs:fluids} -{T':ty}
   +{A:of (tm/app E1 E2) T Cs} -{D:subset Bs Cs} -{B:of E1 (ty/arrow T' T) Bs}
   -{C:of E2 T' Bs} (inv-app A D B C).
%worlds () (inv-app _ _ _ _).
%total T (inv-app T _ _ _).
inv-s :
   {E:tm} {T:ty} {Cs:fluids} {Bs:fluids}
      of (tm/s E) T Cs -> subset Bs Cs -> eqty T ty/nat -> of E ty/nat Bs
         -> type.
- :
   {X1:fluids} {X2:fluids} {X3:fluids} {Sub:subset X1 X2} {Sub':subset X2 X3}
      {Sub'':subset X1 X3} {X4:tm} {X5:ty} {T:of (tm/s X4) X5 X2}
      {Eq:eqty X5 ty/nat} {T':of X4 ty/nat X1}
      subset-trans Sub Sub' Sub'' -> inv-s T Sub Eq T'
         -> inv-s (of/weaken T Sub') Sub'' Eq T'.
- :
   {X1:fluids} {Sub:subset X1 X1} {X2:tm} {T:of X2 ty/nat X1}
      subset-refl X1 Sub -> inv-s (of/s T) Sub eqty/refl T.
%mode +{E:tm} +{T:ty} +{Cs:fluids} -{Bs:fluids} +{A:of (tm/s E) T Cs}
   -{B:subset Bs Cs} -{D:eqty T ty/nat} -{C:of E ty/nat Bs} (inv-s A B D C).
%worlds () (inv-s _ _ _ _).
%total T (inv-s T _ _ _).
inv-if :
   {E:tm} {E1:tm} {E2:tm -> tm} {T:ty} {Cs:fluids} {Bs:fluids}
      of (tm/if E E1 ([x:tm] E2 x)) T Cs -> subset Bs Cs -> of E ty/nat Bs
         -> of E1 T Bs -> ({x:tm} of x ty/nat # -> of (E2 x) T Bs) -> type.
- :
   {X1:fluids} {X2:fluids} {X3:fluids} {Sub:subset X1 X2} {Sub':subset X2 X3}
      {Sub'':subset X1 X3} {X4:tm} {X5:tm} {X6:tm -> tm} {X7:ty}
      {Tif:of (tm/if X4 X5 ([x:tm] X6 x)) X7 X2} {T:of X4 ty/nat X1}
      {T1:of X5 X7 X1} {T2:{x:tm} of x ty/nat # -> of (X6 x) X7 X1}
      subset-trans Sub Sub' Sub''
         -> inv-if Tif Sub T T1 ([x:tm] [x1:of x ty/nat #] T2 x x1)
         -> inv-if (of/weaken Tif Sub') Sub'' T T1
               ([x:tm] [x1:of x ty/nat #] T2 x x1).
- :
   {X1:fluids} {Sub:subset X1 X1} {X2:tm} {X3:tm} {X4:tm -> tm} {X5:ty}
      {T:of X2 ty/nat X1} {T1:of X3 X5 X1}
      {T2:{x:tm} of x ty/nat # -> of (X4 x) X5 X1}
      subset-refl X1 Sub
         -> inv-if (of/if T T1 ([x:tm] [x1:of x ty/nat #] T2 x x1)) Sub T T1
               ([x:tm] [x1:of x ty/nat #] T2 x x1).
%mode +{E:tm} +{E1:tm} +{E2:tm -> tm} +{T:ty} +{Cs:fluids} -{Bs:fluids}
   +{A:of (tm/if E E1 ([x:tm] E2 x)) T Cs} -{B:subset Bs Cs} -{C:of E ty/nat Bs}
   -{D:of E1 T Bs} -{E3:{x:tm} of x ty/nat # -> of (E2 x) T Bs}
   (inv-if A B C D E3).
%worlds () (inv-if _ _ _ _ _).
%total T (inv-if T _ _ _ _).
inv-fix :
   {T':ty} {F:tm -> tm} {T:ty} {Cs:fluids}
      of (tm/fix T' ([x:tm] F x)) T Cs -> eqty T T'
         -> of (tm/fix T ([x:tm] F x)) T # -> ({x:tm} of x T # -> of (F x) T #)
         -> type.
- :
   {X1:ty} {X2:tm -> tm} {X3:ty} {X4:fluids}
      {Tfix:of (tm/fix X1 ([x:tm] X2 x)) X3 X4} {Eq:eqty X3 X1}
      {Tfix':of (tm/fix X3 ([x:tm] X2 x)) X3 #}
      {Tfn:{x:tm} of x X3 # -> of (X2 x) X3 #} {X5:fluids} {Sub:subset X4 X5}
      inv-fix Tfix Eq Tfix' ([x:tm] [x1:of x X3 #] Tfn x x1)
         -> inv-fix (of/weaken Tfix Sub) Eq Tfix'
               ([x:tm] [x1:of x X3 #] Tfn x x1).
- :
   {X1:ty} {X2:tm -> tm} {T:{x:tm} of x X1 # -> of (X2 x) X1 #}
      inv-fix (of/fix ([x:tm] [x1:of x X1 #] T x x1)) eqty/refl
         (of/fix ([x:tm] [x1:of x X1 #] T x x1)) ([x:tm] [x1:of x X1 #] T x x1).
%mode +{T':ty} +{F:tm -> tm} +{T:ty} +{Cs:fluids}
   +{A:of (tm/fix T' ([x:tm] F x)) T Cs} -{B:eqty T T'}
   -{C:of (tm/fix T ([x:tm] F x)) T #} -{D:{x:tm} of x T # -> of (F x) T #}
   (inv-fix A B C D).
%worlds () (inv-fix _ _ _ _).
%total T (inv-fix T _ _ _).
inv-access :
   {A:fluid} {T:ty} {Cs:fluids}
      of (tm/access A) T Cs -> in A Cs -> fluidty A T -> type.
- :
   {X1:fluid} {X2:fluids} {X3:fluids} {In:in X1 X2} {Sub:subset X2 X3}
      {In':in X1 X3} {X4:ty} {Taccess:of (tm/access X1) X4 X2}
      {FT:fluidty X1 X4}
      in-subset In Sub In' -> inv-access Taccess In FT
         -> inv-access (of/weaken Taccess Sub) In' FT.
- : {X1:fluid} {X2:ty} {FT:fluidty X1 X2} inv-access (of/access FT) in/z FT.
%mode +{A:fluid} +{T:ty} +{Cs:fluids} +{A1:of (tm/access A) T Cs} -{B:in A Cs}
   -{C:fluidty A T} (inv-access A1 B C).
%worlds () (inv-access _ _ _).
%total T (inv-access T _ _).
inv-fluid-let :
   {A:fluid} {E1:tm} {E2:tm} {T:ty} {Cs:fluids} {Bs:fluids} {Tf:ty}
      of (tm/fluid-let A E1 E2) T Cs -> subset Bs Cs -> fluidty A Tf
         -> of E1 Tf Bs -> of E2 T (A , Bs) -> type.
- :
   {X1:fluids} {X2:fluids} {X3:fluids} {Sub:subset X1 X2} {Sub':subset X2 X3}
      {Sub'':subset X1 X3} {X4:fluid} {X5:tm} {X6:tm} {X7:ty} {X8:ty}
      {Tfluid:of (tm/fluid-let X4 X5 X6) X7 X2} {FT:fluidty X4 X8}
      {T1:of X5 X8 X1} {T2:of X6 X7 (X4 , X1)}
      subset-trans Sub Sub' Sub'' -> inv-fluid-let Tfluid Sub FT T1 T2
         -> inv-fluid-let (of/weaken Tfluid Sub') Sub'' FT T1 T2.
- :
   {X1:fluids} {Sub:subset X1 X1} {X2:fluid} {X3:tm} {X4:tm} {X5:ty} {X6:ty}
      {FT:fluidty X2 X6} {T1:of X3 X6 X1} {T2:of X4 X5 (X2 , X1)}
      subset-refl X1 Sub -> inv-fluid-let (of/fluid-let FT T1 T2) Sub FT T1 T2.
%mode +{A:fluid} +{E1:tm} +{E2:tm} +{T:ty} +{Cs:fluids} -{Bs:fluids} -{Tf:ty}
   +{A1:of (tm/fluid-let A E1 E2) T Cs} -{B:subset Bs Cs} -{C:fluidty A Tf}
   -{D:of E1 Tf Bs} -{E:of E2 T (A , Bs)} (inv-fluid-let A1 B C D E).
%worlds () (inv-fluid-let _ _ _ _ _).
%total T (inv-fluid-let T _ _ _ _).
inv-unsusp :
   {E:tm} {T:ty} {Ds:fluids} {Cs:fluids} {As:fluids} {Bs:fluids}
      of (tm/unsusp E) T Ds -> subset Cs Ds -> of E (ty/mayuse T As) Bs
         -> merge As Bs Cs -> type.
- :
   {X1:fluids} {X2:fluids} {X3:fluids} {Sub:subset X1 X2} {Sub':subset X2 X3}
      {Sub'':subset X1 X3} {X4:tm} {X5:ty} {X6:fluids} {X7:fluids}
      {Tun:of (tm/unsusp X4) X5 X2} {T:of X4 (ty/mayuse X5 X6) X7}
      {M:merge X6 X7 X1}
      subset-trans Sub Sub' Sub'' -> inv-unsusp Tun Sub T M
         -> inv-unsusp (of/weaken Tun Sub') Sub'' T M.
- :
   {X1:fluids} {Sub:subset X1 X1} {X2:tm} {X3:ty} {X4:fluids} {X5:fluids}
      {Merge:merge X4 X5 X1} {T:of X2 (ty/mayuse X3 X4) X5}
      subset-refl X1 Sub -> inv-unsusp (of/unsusp Merge T) Sub T Merge.
%mode +{E:tm} +{T:ty} +{Ds:fluids} -{Cs:fluids} -{As:fluids} -{Bs:fluids}
   +{A:of (tm/unsusp E) T Ds} -{B:subset Cs Ds} -{C:of E (ty/mayuse T As) Bs}
   -{D:merge As Bs Cs} (inv-unsusp A B C D).
%worlds () (inv-unsusp _ _ _ _).
%total T (inv-unsusp T _ _ _).
invf-app1 :
   {E2:tm} {K:stack} {T:ty} {Bs:fluids} {Cs:fluids} {T1:ty} {T2:ty}
      ofstack (f/app1 --- E2 ; K) T Bs -> subset Bs Cs
         -> eqty T (ty/arrow T1 T2) -> ofstack K T2 Cs -> of E2 T1 Cs -> type.
- :
   {As:fluids} {Bs:fluids} {Cs:fluids} {Sub:subset As Bs} {Sub':subset Bs Cs}
      {Sub'':subset As Cs} {X1:tm} {X2:stack} {X3:ty} {X4:ty} {X5:ty}
      {TK:ofstack (f/app1 --- X1 ; X2) X3 Bs} {Eq:eqty X3 (ty/arrow X4 X5)}
      {TK':ofstack X2 X5 Cs} {TE':of X1 X4 Cs}
      subset-trans Sub Sub' Sub'' -> invf-app1 TK Sub' Eq TK' TE'
         -> invf-app1 (ofstack/weaken TK Sub) Sub'' Eq TK' TE'.
- :
   {Cs:fluids} {Sub:subset Cs Cs} {E2:tm} {K:stack} {T1:ty} {T2:ty}
      {TE:of E2 T1 Cs} {TK:ofstack K T2 Cs}
      subset-refl Cs Sub
         -> invf-app1 (ofstack/frame (offrame/app1 TE) TK) Sub eqty/refl TK TE.
%mode +{E2:tm} +{K:stack} +{T:ty} +{Bs:fluids} -{Cs:fluids} -{T1:ty} -{T2:ty}
   +{A:ofstack (f/app1 --- E2 ; K) T Bs} -{E:subset Bs Cs}
   -{B:eqty T (ty/arrow T1 T2)} -{C:ofstack K T2 Cs} -{D:of E2 T1 Cs}
   (invf-app1 A E B C D).
%worlds () (invf-app1 _ _ _ _ _).
%total T (invf-app1 T _ _ _ _).
invf-app2 :
   {E1:tm} {Dv:v E1} {K:stack} {Targ:ty} {Bs:fluids} {Cs:fluids} {Tres:ty}
      ofstack (f/app2 E1 Dv --- ; K) Targ Bs -> subset Bs Cs
         -> of E1 (ty/arrow Targ Tres) Cs -> ofstack K Tres Cs -> type.
- :
   {X1:fluids} {X2:fluids} {X3:fluids} {Sub:subset X1 X2} {Sub':subset X2 X3}
      {Sub'':subset X1 X3} {X4:tm} {X5:v X4} {X6:stack} {X7:ty} {X8:ty}
      {TK:ofstack (f/app2 X4 X5 --- ; X6) X7 X2} {TE':of X4 (ty/arrow X7 X8) X3}
      {TK':ofstack X6 X8 X3}
      subset-trans Sub Sub' Sub'' -> invf-app2 TK Sub' TE' TK'
         -> invf-app2 (ofstack/weaken TK Sub) Sub'' TE' TK'.
- :
   {X1:fluids} {Sub:subset X1 X1} {X2:tm} {X3:v X2} {X4:stack} {X5:ty} {X6:ty}
      {TE:of X2 (ty/arrow X5 X6) #} {TK:ofstack X4 X6 X1}
      subset-refl X1 Sub
         -> invf-app2 (ofstack/frame (offrame/app2 TE) TK) Sub
               (of/weaken TE subset/z) TK.
%mode +{E1:tm} +{Dv:v E1} +{K:stack} +{Targ:ty} +{Bs:fluids} -{Cs:fluids} -{Tres:ty}
   +{A:ofstack (f/app2 E1 Dv --- ; K) Targ Bs} -{B:subset Bs Cs}
   -{C:of E1 (ty/arrow Targ Tres) Cs} -{D:ofstack K Tres Cs} (invf-app2 A B C D).
%worlds () (invf-app2 _ _ _ _).
%total T (invf-app2 T _ _ _).
invf-s :
   {K:stack} {T:ty} {Bs:fluids} {Cs:fluids}
      ofstack (f/s --- ; K) T Bs -> subset Bs Cs -> eqty T ty/nat
         -> ofstack K ty/nat Cs -> type.
- :
   {X1:fluids} {X2:fluids} {X3:fluids} {Sub:subset X1 X2} {Sub':subset X2 X3}
      {Sub'':subset X1 X3} {X4:stack} {X5:ty} {TK:ofstack (f/s --- ; X4) X5 X2}
      {Eq:eqty X5 ty/nat} {TK':ofstack X4 ty/nat X3}
      subset-trans Sub Sub' Sub'' -> invf-s TK Sub' Eq TK'
         -> invf-s (ofstack/weaken TK Sub) Sub'' Eq TK'.
- :
   {X1:fluids} {Sub:subset X1 X1} {X2:stack} {TK:ofstack X2 ty/nat X1}
      subset-refl X1 Sub -> invf-s (ofstack/frame offrame/s TK) Sub eqty/refl TK.
%mode +{K:stack} +{T:ty} +{Bs:fluids} -{Cs:fluids} +{A:ofstack (f/s --- ; K) T Bs}
   -{B:subset Bs Cs} -{C:eqty T ty/nat} -{D:ofstack K ty/nat Cs}
   (invf-s A B C D).
%worlds () (invf-s _ _ _ _).
%total T (invf-s T _ _ _).
invf-if :
   {E1:tm} {E2:tm -> tm} {K:stack} {Tn:ty} {Bs:fluids} {Cs:fluids} {T:ty}
      ofstack (f/if --- E1 ([x:tm] E2 x) ; K) Tn Bs -> subset Bs Cs
         -> eqty Tn ty/nat -> of E1 T Cs
         -> ({x:tm} of x ty/nat # -> of (E2 x) T Cs) -> ofstack K T Cs -> type.
- :
   {X1:fluids} {X2:fluids} {X3:fluids} {Sub:subset X1 X2} {Sub':subset X2 X3}
      {Sub'':subset X1 X3} {X4:tm} {X5:tm -> tm} {X6:stack} {X7:ty} {X8:ty}
      {TK:ofstack (f/if --- X4 ([x:tm] X5 x) ; X6) X7 X2} {Eq:eqty X7 ty/nat}
      {TE1:of X4 X8 X3} {TE2:{x:tm} of x ty/nat # -> of (X5 x) X8 X3}
      {TK':ofstack X6 X8 X3}
      subset-trans Sub Sub' Sub''
         -> invf-if TK Sub' Eq TE1 ([x:tm] [x1:of x ty/nat #] TE2 x x1) TK'
         -> invf-if (ofstack/weaken TK Sub) Sub'' Eq TE1
               ([x:tm] [x1:of x ty/nat #] TE2 x x1) TK'.
- :
   {X1:fluids} {Sub:subset X1 X1} {X2:tm} {X3:tm -> tm} {X4:stack} {X5:ty}
      {T1:of X2 X5 X1} {T2:{x:tm} of x ty/nat # -> of (X3 x) X5 X1}
      {TK:ofstack X4 X5 X1}
      subset-refl X1 Sub
         -> invf-if
               (ofstack/frame
                   (offrame/if T1 ([x:tm] [x1:of x ty/nat #] T2 x x1)) TK) Sub
               eqty/refl T1 ([x:tm] [x1:of x ty/nat #] T2 x x1) TK.
%mode +{E1:tm} +{E2:tm -> tm} +{K:stack} +{Tn:ty} +{Bs:fluids} -{Cs:fluids} -{T:ty}
   +{A:ofstack (f/if --- E1 ([x:tm] E2 x) ; K) Tn Bs} -{B:subset Bs Cs}
   -{C:eqty Tn ty/nat} -{D:of E1 T Cs}
   -{E:{x:tm} of x ty/nat # -> of (E2 x) T Cs} -{F:ofstack K T Cs}
   (invf-if A B C D E F).
%worlds () (invf-if _ _ _ _ _ _).
%total T (invf-if T _ _ _ _ _).
invf-fluid-let :
   {A:fluid} {E2:tm} {K:stack} {Tf:ty} {Bs:fluids} {Cs:fluids} {T:ty}
      ofstack (f/fluid-let A --- E2 ; K) Tf Bs -> subset Bs Cs -> fluidty A Tf
         -> of E2 T (A , Cs) -> ofstack K T Cs -> type.
- :
   {X1:fluids} {X2:fluids} {X3:fluids} {Sub:subset X1 X2} {Sub':subset X2 X3}
      {Sub'':subset X1 X3} {X4:fluid} {X5:tm} {X6:stack} {X7:ty} {X8:ty}
      {TK:ofstack (f/fluid-let X4 --- X5 ; X6) X7 X2} {TF:fluidty X4 X7}
      {T2:of X5 X8 (X4 , X3)} {TK':ofstack X6 X8 X3}
      subset-trans Sub Sub' Sub'' -> invf-fluid-let TK Sub' TF T2 TK'
         -> invf-fluid-let (ofstack/weaken TK Sub) Sub'' TF T2 TK'.
- :
   {X1:fluids} {Sub:subset X1 X1} {X2:fluid} {X3:tm} {X4:stack} {X5:ty} {X6:ty}
      {FT:fluidty X2 X5} {T2:of X3 X6 (X2 , X1)} {TK:ofstack X4 X6 X1}
      subset-refl X1 Sub
         -> invf-fluid-let (ofstack/frame (offrame/fluid-let FT T2) TK) Sub FT
               T2 TK.
%mode +{A:fluid} +{E2:tm} +{K:stack} +{Tf:ty} +{Bs:fluids} -{Cs:fluids} -{T:ty}
   +{A1:ofstack (f/fluid-let A --- E2 ; K) Tf Bs} -{B:subset Bs Cs}
   -{C:fluidty A Tf} -{D:of E2 T (A , Cs)} -{E:ofstack K T Cs}
   (invf-fluid-let A1 B C D E).
%worlds () (invf-fluid-let _ _ _ _ _).
%total T (invf-fluid-let T _ _ _ _).
invf-fluid-bind :
   {A:fluid} {E:tm} {Dv:v E} {K:stack} {T:ty} {Bs:fluids} {Cs:fluids}
      ofstack (f/fluid-bind A E Dv ; K) T Bs -> subset Bs (A , Cs)
         -> ofstack K T Cs -> type.
- :
   {X1:fluids} {X2:fluids} {X3:fluid} {X4:fluids} {Sub:subset X1 X2}
      {Sub':subset X2 (X3 , X4)} {Sub'':subset X1 (X3 , X4)} {X5:tm} {X6:v X5}
      {X7:stack} {X8:ty} {TK:ofstack (f/fluid-bind X3 X5 X6 ; X7) X8 X2}
      {TK':ofstack X7 X8 X4}
      subset-trans Sub Sub' Sub'' -> invf-fluid-bind TK Sub' TK'
         -> invf-fluid-bind (ofstack/weaken TK Sub) Sub'' TK'.
- :
   {X1:fluids} {X2:fluid} {Sub:subset X1 X1} {Sub':subset X1 (X2 , X1)} {X3:tm}
      {X4:v X3} {X5:stack} {X6:ty} {X7:ty} {X8:fluidty X2 X7} {X9:of X3 X7 #}
      {TK:ofstack X5 X6 X1}
      subset-weaken X2 Sub Sub' -> subset-refl X1 Sub
         -> invf-fluid-bind (ofstack/frame (offrame/fluid-bind X8 X9) TK)
               (subset/s in/z Sub') TK.
%mode +{A:fluid} +{E:tm} +{Dv:v E} +{K:stack} +{T:ty} +{Bs:fluids} -{Cs:fluids}
   +{A1:ofstack (f/fluid-bind A E Dv ; K) T Bs} -{B:subset Bs (A , Cs)}
   -{C:ofstack K T Cs} (invf-fluid-bind A1 B C).
%worlds () (invf-fluid-bind _ _ _).
%total T (invf-fluid-bind T _ _).
preservation : {S:state} {S':state} step S S' -> ok S -> ok S' -> type.
%mode +{S:state} +{S':state} +{A:step S S'} +{B:ok S} -{C:ok S'} (preservation A B C).
- :
   {X1:stack} {X2:ty} {X3:tm -> tm} {X4:ty} {X5:fluids} {TK:ofstack X1 X4 X5}
      {TE:of (tm/lam X2 ([x:tm] X3 x)) X4 X5}
      preservation step/lam (ok>> TK TE) (ok<< TK TE v/lam).
- :
   {X1:tm} {X2:tm} {X3:ty} {X4:fluids} {X5:fluids} {X6:ty}
      {TE:of (tm/app X1 X2) X3 X4} {Sub:subset X5 X4}
      {T1:of X1 (ty/arrow X6 X3) X5} {T2:of X2 X6 X5} {X7:stack}
      {TK:ofstack X7 X3 X4}
      inv-app TE Sub T1 T2
         -> preservation step/app1 (ok>> TK TE)
               (ok>> (ofstack/frame (offrame/app1 T2) (ofstack/weaken TK Sub))
                   T1).
p1 :
   {T:ty} {T1:ty} {T2:ty} {E:tm} {Bs:fluids}
      eqty T (ty/arrow T1 T2) -> of E T Bs -> of E (ty/arrow T1 T2) Bs -> type.
- :
   {X1:ty} {X2:ty} {X3:tm} {X4:fluids} {T:of X3 (ty/arrow X1 X2) X4}
      p1 eqty/refl T T.
%mode +{T:ty} +{T1:ty} +{T2:ty} +{E:tm} +{Bs:fluids} +{A:eqty T (ty/arrow T1 T2)}
   +{B:of E T Bs} -{C:of E (ty/arrow T1 T2) Bs} (p1 A B C).
%worlds () (p1 _ _ _).
%total {} (p1 _ _ _).
- :
   {E1:tm} {T1:ty} {T2:ty} {Bs:fluids} {Dv:v E1}
      {TE1':of E1 (ty/arrow T1 T2) Bs} {TE1'':of E1 (ty/arrow T1 T2) #} {T:ty}
      {Eq:eqty T (ty/arrow T1 T2)} {TE:of E1 T Bs} {E2:tm} {K:stack} {Cs:fluids}
      {TK:ofstack (f/app1 --- E2 ; K) T Bs} {Sub:subset Bs Cs}
      {TK':ofstack K T2 Cs} {TE2':of E2 T1 Cs}
      effect-value Dv TE1' TE1'' -> p1 Eq TE TE1'
         -> invf-app1 TK Sub Eq TK' TE2'
         -> preservation step/app2 (ok<< TK TE Dv)
               (ok>> (ofstack/frame (offrame/app2 TE1'') TK') TE2').
p3 :
   {Ta:ty} {Tb:ty} {T':ty} {T'':ty} {K:stack} {Cs:fluids} {E:tm -> tm} {E2:tm}
      eqty (ty/arrow Ta Tb) (ty/arrow T' T'') -> ofstack K Tb Cs
         -> ({x:tm} of x T' # -> of (E x) T'' #) -> of E2 Ta #
         -> ok (>> K (E E2)) -> type.
- :
   {X1:ty} {X2:ty} {X3:stack} {X4:fluids} {X5:tm -> tm} {X6:tm}
      {TK:ofstack X3 X2 X4} {TE1:{x:tm} of x X1 # -> of (X5 x) X2 #}
      {TE2:of X6 X1 #}
      p3 eqty/refl TK ([x:tm] [x1:of x X1 #] TE1 x x1) TE2
         (ok>> TK (of/weaken (TE1 X6 TE2) subset/z)).
%mode +{Ta:ty} +{Tb:ty} +{T':ty} +{T'':ty} +{K:stack} +{Cs:fluids} +{E:tm -> tm}
   +{E2:tm} +{A:eqty (ty/arrow Ta Tb) (ty/arrow T' T'')} +{B:ofstack K Tb Cs}
   +{C:{x:tm} of x T' # -> of (E x) T'' #} +{D:of E2 Ta #}
   -{E1:ok (>> K (E E2))} (p3 A B C D E1).
%worlds () (p3 _ _ _ _ _).
%total {} (p3 _ _ _ _ _).
- :
   {Ta:ty} {Tb:ty} {T':ty} {T'':ty} {K:stack} {Cs:fluids} {E:tm -> tm} {E2:tm}
      {Eq:eqty (ty/arrow Ta Tb) (ty/arrow T' T'')} {TK'':ofstack K Tb Cs}
      {Tfunc:{x:tm} of x T' # -> of (E x) T'' #} {TE2':of E2 Ta #}
      {Ans:ok (>> K (E E2))}
      {T1:of (tm/lam T' ([x:tm] E x)) (ty/arrow Ta Tb) Cs}
      {V:v (tm/lam T' ([x:tm] E x))} {Bs:fluids}
      {TK:ofstack (f/app2 (tm/lam T' ([x:tm] E x)) V --- ; K) Ta Bs}
      {Sub:subset Bs Cs} {Dv:v E2} {TE2:of E2 Ta Bs}
      p3 Eq TK'' ([x:tm] [x1:of x T' #] Tfunc x x1) TE2' Ans
         -> inv-lam T1 Eq ([x:tm] [x1:of x T' #] Tfunc x x1)
         -> invf-app2 TK Sub T1 TK'' -> effect-value Dv TE2 TE2'
         -> preservation step/appr (ok<< TK TE2 Dv) Ans.
- :
   {X1:stack} {X2:ty} {X3:fluids} {TK:ofstack X1 X2 X3} {TE:of tm/z X2 X3}
      preservation step/z (ok>> TK TE) (ok<< TK TE v/z).
p2 :
   {T:ty} {K:stack} {Bs:fluids}
      eqty T ty/nat -> ofstack K T Bs -> ofstack K ty/nat Bs -> type.
- : {X1:stack} {X2:fluids} {T:ofstack X1 ty/nat X2} p2 eqty/refl T T.
%mode +{T:ty} +{K:stack} +{Bs:fluids} +{A:eqty T ty/nat} +{B:ofstack K T Bs}
   -{C:ofstack K ty/nat Bs} (p2 A B C).
%worlds () (p2 _ _ _).
%total {} (p2 _ _ _).
- :
   {T:ty} {E:stack} {Bs:fluids} {Eq:eqty T ty/nat} {TK:ofstack E T Bs}
      {TK':ofstack E ty/nat Bs} {X1:tm} {X2:fluids} {TE:of (tm/s X1) T Bs}
      {Sub:subset X2 Bs} {TE':of X1 ty/nat X2}
      p2 Eq TK TK' -> inv-s TE Sub Eq TE'
         -> preservation step/s (ok>> TK TE)
               (ok>> (ofstack/frame offrame/s (ofstack/weaken TK' Sub)) TE').
p6 :
   {T:ty} {E:tm} {Bs:fluids}
      eqty T ty/nat -> of E T Bs -> of E ty/nat Bs -> type.
- : {X1:tm} {X2:fluids} {T:of X1 ty/nat X2} p6 eqty/refl T T.
%mode +{T:ty} +{E:tm} +{Bs:fluids} +{A:eqty T ty/nat} +{B:of E T Bs}
   -{C:of E ty/nat Bs} (p6 A B C).
%worlds () (p6 _ _ _).
%total {} (p6 _ _ _).
- :
   {T:ty} {X1:tm} {Bs:fluids} {Eq:eqty T ty/nat} {TE:of X1 T Bs}
      {TE':of X1 ty/nat Bs} {K:stack} {Cs:fluids}
      {TK:ofstack (f/s --- ; K) T Bs} {Sub:subset Bs Cs}
      {TK':ofstack K ty/nat Cs} {Dv:v X1}
      p6 Eq TE TE' -> invf-s TK Sub Eq TK'
         -> preservation step/sr (ok<< TK TE Dv)
               (ok<< TK' (of/weaken (of/s TE') Sub) (v/s Dv)).
- :
   {X1:tm} {X2:tm} {X3:tm -> tm} {X4:ty} {X5:fluids} {X6:fluids}
      {TE:of (tm/if X1 X2 ([x:tm] X3 x)) X4 X5} {Sub:subset X6 X5}
      {T:of X1 ty/nat X6} {T1:of X2 X4 X6}
      {T2:{x:tm} of x ty/nat # -> of (X3 x) X4 X6} {X7:stack}
      {TK:ofstack X7 X4 X5}
      inv-if TE Sub T T1 ([x:tm] [x1:of x ty/nat #] T2 x x1)
         -> preservation step/if (ok>> TK TE)
               (ok>>
                   (ofstack/frame
                       (offrame/if T1 ([x:tm] [x1:of x ty/nat #] T2 x x1))
                       (ofstack/weaken TK Sub)) T).
- :
   {E1:tm} {E2:tm -> tm} {K:stack} {T:ty} {Bs:fluids} {Cs:fluids} {T':ty}
      {TK:ofstack (f/if --- E1 ([x:tm] E2 x) ; K) T Bs} {Sub:subset Bs Cs}
      {Eq:eqty T ty/nat} {TE1:of E1 T' Cs}
      {X1:{x:tm} of x ty/nat # -> of (E2 x) T' Cs} {TK':ofstack K T' Cs}
      {Dv:v tm/z} {TE:of tm/z T Bs}
      invf-if TK Sub Eq TE1 ([x:tm] [x1:of x ty/nat #] X1 x x1) TK'
         -> preservation step/ifz (ok<< TK TE Dv) (ok>> TK' TE1).
- :
   {N:tm} {T:ty} {As:fluids} {TE':of (tm/s N) T #} {Sub#:subset As #}
      {X1:eqty T ty/nat} {TN:of N ty/nat As} {Bs:fluids} {Dv:v (tm/s N)}
      {TE:of (tm/s N) T Bs} {E1:tm} {E2:tm -> tm} {K:stack} {Cs:fluids} {T':ty}
      {TK:ofstack (f/if --- E1 ([x:tm] E2 x) ; K) T Bs} {Sub:subset Bs Cs}
      {Eq:eqty T ty/nat} {X2:of E1 T' Cs}
      {TE2:{x:tm} of x ty/nat # -> of (E2 x) T' Cs} {TK':ofstack K T' Cs}
      inv-s TE' Sub# X1 TN -> effect-value Dv TE TE'
         -> invf-if TK Sub Eq X2 ([x:tm] [x1:of x ty/nat #] TE2 x x1) TK'
         -> preservation step/ifs (ok<< TK TE Dv)
               (ok>> TK' (TE2 N (of/weaken TN Sub#))).
p6 :
   {T:ty} {T':ty} {F:tm -> tm}
      eqty T T' -> of (tm/fix T ([x:tm] F x)) T #
         -> ({x:tm} of x T # -> of (F x) T #) -> of (tm/fix T' ([x:tm] F x)) T 
#
         -> ({x:tm} of x T # -> of (F x) T #) -> type.
- :
   {X1:ty} {X2:tm -> tm} {T:of (tm/fix X1 ([x:tm] X2 x)) X1 #}
      {F:{x:tm} of x X1 # -> of (X2 x) X1 #}
      p6 eqty/refl T ([x:tm] [x1:of x X1 #] F x x1) T
         ([x:tm] [x1:of x X1 #] F x x1).
%mode +{T:ty} +{T':ty} +{F:tm -> tm} +{A:eqty T T'}
   +{B:of (tm/fix T ([x:tm] F x)) T #} +{C:{x:tm} of x T # -> of (F x) T #}
   -{D:of (tm/fix T' ([x:tm] F x)) T #} -{E:{x:tm} of x T # -> of (F x) T #}
   (p6 A B C D E).
%worlds () (p6 _ _ _ _ _).
%total {} (p6 _ _ _ _ _).
- :
   {T:ty} {T':ty} {F:tm -> tm} {Eq:eqty T T'}
      {Tfix:of (tm/fix T ([x:tm] F x)) T #}
      {Tfn:{x:tm} of x T # -> of (F x) T #}
      {Tfix':of (tm/fix T' ([x:tm] F x)) T #}
      {Tfn':{x:tm} of x T # -> of (F x) T #} {Bs:fluids}
      {TE:of (tm/fix T' ([x:tm] F x)) T Bs} {X1:stack} {TK:ofstack X1 T Bs}
      p6 Eq Tfix ([x:tm] [x1:of x T #] Tfn x x1) Tfix'
         ([x:tm] [x1:of x T #] Tfn' x x1)
         -> inv-fix TE Eq Tfix ([x:tm] [x1:of x T #] Tfn x x1)
         -> preservation step/fix (ok>> TK TE)
               (ok>> TK
                   (of/weaken (Tfn' (tm/fix T' ([x:tm] F x)) Tfix') subset/z)).
p5 : {T:ty} {T':ty} {E:tm} eqty T T' -> of E T # -> of E T' # -> type.
- : {X1:ty} {X2:tm} {T:of X2 X1 #} p5 eqty/refl T T.
%mode +{T:ty} +{T':ty} +{E:tm} +{A:eqty T T'} +{B:of E T #} -{C:of E T' #} (p5 A B C).
%worlds () (p5 _ _ _).
%total {} (p5 _ _ _).
- :
   {T':ty} {T:ty} {V:tm} {Eq:eqty T' T} {TE':of V T' #} {TE'':of V T #}
      {A:fluid} {FT':fluidty A T'} {FT:fluidty A T} {Bs:fluids} {K:stack}
      {Dv:v V} {In:in A Bs} {TK:ofstack K T Bs} {Look:lookup A K V Dv}
      {TE:of (tm/access A) T Bs}
      p5 Eq TE' TE'' -> fluidty-uniq FT' FT Eq
         -> access-stack' In TK Look FT' TE' -> inv-access TE In FT
         -> preservation (step/access Look) (ok>> TK TE)
               (ok<< TK (of/weaken TE'' subset/z) Dv).
- :
   {A:fluid} {E1:tm} {E2:tm} {T:ty} {Cs:fluids} {Bs:fluids} {Tf:ty}
      {TE:of (tm/fluid-let A E1 E2) T Cs} {Sub:subset Bs Cs} {FT:fluidty A Tf}
      {T1:of E1 Tf Bs} {T2:of E2 T (A , Bs)} {X1:stack} {TK:ofstack X1 T Cs}
      inv-fluid-let TE Sub FT T1 T2
         -> preservation step/flet1 (ok>> TK TE)
               (ok>>
                   (ofstack/frame (offrame/fluid-let FT T2)
                       (ofstack/weaken TK Sub)) T1).
- :
   {E1:tm} {Tf:ty} {Bs:fluids} {Dv:v E1} {TE:of E1 Tf Bs} {TE':of E1 Tf #}
      {A:fluid} {E2:tm} {K:stack} {Cs:fluids} {T:ty}
      {TK:ofstack (f/fluid-let A --- E2 ; K) Tf Bs} {Sub:subset Bs Cs}
      {FT:fluidty A Tf} {T2:of E2 T (A , Cs)} {TK':ofstack K T Cs}
      effect-value Dv TE TE' -> invf-fluid-let TK Sub FT T2 TK'
         -> preservation step/flet2 (ok<< TK TE Dv)
               (ok>> (ofstack/frame (offrame/fluid-bind FT TE') TK') T2).
- :
   {X1:fluid} {X2:tm} {X3:v X2} {X4:stack} {X5:ty} {X6:fluids} {X7:fluids}
      {TK:ofstack (f/fluid-bind X1 X2 X3 ; X4) X5 X6} {X8:subset X6 (X1 , X7)}
      {TK':ofstack X4 X5 X7} {X9:tm} {Dv:v X9} {TE:of X9 X5 X6} {TE':of X9 X5 #}
      invf-fluid-bind TK X8 TK' -> effect-value Dv TE TE'
         -> preservation step/fletr (ok<< TK TE Dv)
               (ok<< TK' (of/weaken TE' subset/z) Dv).
- :
   {X1:stack} {X2:tm} {X3:ty} {X4:fluids} {TK:ofstack X1 X3 X4}
      {TE:of (tm/susp X2) X3 X4}
      preservation step/susp (ok>> TK TE) (ok<< TK TE v/susp).
- :
   {E:tm} {T:ty} {Ds:fluids} {Cs:fluids} {As:fluids} {Bs:fluids}
      {TE:of (tm/unsusp E) T Ds} {Sub:subset Cs Ds}
      {TE':of E (ty/mayuse T As) Bs} {Merge:merge As Bs Cs} {K:stack}
      {TK:ofstack K T Ds}
      inv-unsusp TE Sub TE' Merge
         -> preservation step/ususp (ok>> TK TE)
               (ok>>
                   (ofstack/frame (offrame/unsusp Merge) (ofstack/weaken TK Sub))
                   TE').
inv-susp :
   {E:tm} {T:ty} {Cs:fluids} {T':ty} {As:fluids}
      of (tm/susp E) T Cs -> eqty T (ty/mayuse T' As)
         -> of (tm/susp E) (ty/mayuse T' As) # -> of E T' As -> type.
- :
   {X1:tm} {X2:ty} {X3:fluids} {X4:ty} {X5:fluids} {Ts:of (tm/susp X1) X2 X3}
      {Eq:eqty X2 (ty/mayuse X4 X5)} {Ts':of (tm/susp X1) (ty/mayuse X4 X5) #}
      {T:of X1 X4 X5} {X6:fluids} {Sub:subset X3 X6}
      inv-susp Ts Eq Ts' T -> inv-susp (of/weaken Ts Sub) Eq Ts' T.
- :
   {X1:tm} {X2:ty} {X3:fluids} {T:of X1 X2 X3}
      inv-susp (of/susp T) eqty/refl (of/susp T) T.
%mode +{E:tm} +{T:ty} +{Cs:fluids} -{T':ty} -{As:fluids} +{A:of (tm/susp E) T Cs}
   -{B:eqty T (ty/mayuse T' As)} -{C:of (tm/susp E) (ty/mayuse T' As) #}
   -{D:of E T' As} (inv-susp A B C D).
%worlds () (inv-susp _ _ _ _).
%total T (inv-susp T _ _ _).
invf-unsusp :
   {K:stack} {T:ty} {B's:fluids} {Bs:fluids} {T':ty} {As:fluids} {Cs:fluids}
      ofstack (f/unsusp --- ; K) T B's -> subset B's Bs
         -> eqty T (ty/mayuse T' As) -> merge As Bs Cs -> ofstack K T' Cs
         -> type.
- :
   {X1:fluids} {X2:fluids} {Bs:fluids} {Sub:subset X1 X2} {Sub':subset X2 Bs}
      {Sub'':subset X1 Bs} {X3:stack} {X4:ty} {X5:ty} {As:fluids} {Cs:fluids}
      {TK:ofstack (f/unsusp --- ; X3) X4 X2} {Eq:eqty X4 (ty/mayuse X5 As)}
      {Merge:merge As Bs Cs} {TK':ofstack X3 X5 Cs}
      subset-trans Sub Sub' Sub'' -> invf-unsusp TK Sub' Eq Merge TK'
         -> invf-unsusp (ofstack/weaken TK Sub) Sub'' Eq Merge TK'.
- :
   {Bs:fluids} {Sub:subset Bs Bs} {K:stack} {T:ty} {As:fluids} {Cs:fluids}
      {Merge:merge As Bs Cs} {TK:ofstack K T Cs}
      subset-refl Bs Sub
         -> invf-unsusp (ofstack/frame (offrame/unsusp Merge) TK) Sub eqty/refl
               Merge TK.
%mode +{K:stack} +{T:ty} +{B's:fluids} -{Bs:fluids} -{T':ty} -{As:fluids} -{Cs:fluids}
   +{A:ofstack (f/unsusp --- ; K) T B's} -{B:subset B's Bs}
   -{C:eqty T (ty/mayuse T' As)} -{D:merge As Bs Cs} -{E:ofstack K T' Cs}
   (invf-unsusp A B C D E).
%worlds () (invf-unsusp _ _ _ _ _).
%total T (invf-unsusp T _ _ _ _).
p7 :
   {T:ty} {T':ty} {As:fluids} {T'':ty} {As':fluids} {K:stack} {Cs:fluids}
      eqty T (ty/mayuse T' As) -> eqty T (ty/mayuse T'' As') -> ofstack K T'' Cs
         -> ofstack K T' Cs -> type.
- :
   {X1:ty} {X2:fluids} {X3:stack} {X4:fluids} {T:ofstack X3 X1 X4}
      p7 eqty/refl eqty/refl T T.
%mode +{T:ty} +{T':ty} +{As:fluids} +{T'':ty} +{As':fluids} +{K:stack} +{Cs:fluids}
   +{A:eqty T (ty/mayuse T' As)} +{B:eqty T (ty/mayuse T'' As')}
   +{C:ofstack K T'' Cs} -{D:ofstack K T' Cs} (p7 A B C D).
%worlds () (p7 _ _ _ _).
%total {} (p7 _ _ _ _).
p8 :
   {T:ty} {T':ty} {As:fluids} {T'':ty} {As':fluids} {B's:fluids} {Cs:fluids}
      eqty T (ty/mayuse T' As) -> eqty T (ty/mayuse T'' As') -> merge As' B's Cs
         -> merge As B's Cs -> type.
- :
   {X1:ty} {X2:fluids} {X3:fluids} {X4:fluids} {T:merge X2 X3 X4}
      p8 eqty/refl eqty/refl T T.
%mode +{T:ty} +{T':ty} +{As:fluids} +{T'':ty} +{As':fluids} +{B's:fluids} +{Cs:fluids}
   +{A:eqty T (ty/mayuse T' As)} +{B:eqty T (ty/mayuse T'' As')}
   +{C:merge As' B's Cs} -{D:merge As B's Cs} (p8 A B C D).
%worlds () (p8 _ _ _ _).
%total {} (p8 _ _ _ _).
- :
   {As:fluids} {B's:fluids} {Cs:fluids} {Merge':merge As B's Cs}
      {Sub:subset As Cs} {T:ty} {T':ty} {T'':ty} {As':fluids}
      {Eq:eqty T (ty/mayuse T' As)} {Eq2:eqty T (ty/mayuse T'' As')}
      {Merge:merge As' B's Cs} {K:stack} {TK':ofstack K T'' Cs}
      {TK'':ofstack K T' Cs} {Bs:fluids} {TK:ofstack (f/unsusp --- ; K) T Bs}
      {Sub':subset Bs B's} {E:tm} {TE:of (tm/susp E) T Bs}
      {X1:of (tm/susp E) (ty/mayuse T' As) #} {TE':of E T' As}
      {Dv:v (tm/susp E)}
      merge-subset1 Merge' Sub -> p8 Eq Eq2 Merge Merge' -> p7 Eq Eq2 TK' TK''
         -> invf-unsusp TK Sub' Eq2 Merge TK' -> inv-susp TE Eq X1 TE'
         -> preservation step/ususpr (ok<< TK TE Dv)
               (ok>> (ofstack/weaken TK'' Sub) TE').
%worlds () (preservation _ _ _).
%total {} (preservation _ _ _).
[Closing file /home/www/twelf/hcode/23781ba1f02ec25cd76458f6614433c7]
%% OK %%