THEOREM[preservation]
    If C = D;G;P;L and |- C and C |- prog and (L;prog) --> (L';prog')
    then |- C' and C' |- prog' where C' = D;G;P;L'
Follows from:
(1) If |- C and C |- e:t and e --> e'
    then C |- e':t
(2) If C = D;G;P;L and |- C and C |- c:t and c --> c'
    then C |- c':t
(3) If C = D;G;P;Lp and |- C,Ls and C |- prog
    and Ls,Lp;prog --> L';prog'
    then |- C',Ls and C' |- prog'
    where C' = D;G;P;Lp' and L'=Ls,Lp' for some Lp'

Proof by induction on the typing derivation.  See below.

THEOREM[progress]
    If C = {};{};P;L and |- C and C |- prog
    then there is some L';prog' such that L;prog --> L';prog'
Follows from:
(1) If C = {};{};P;L and |- C and C |- e:t and e is not a value
    then there is some e' such that e --> e'
(2) If C = {};{};P;L and |- C and C |- c:t and c is not a value
    then there is some c' such that c --> c'
(3) If C = {};{};P;Lp and |- C,Ls and C |- prog
    then there is some L';prog' such that Ls,Lp;prog --> Ls,Lp';prog'

Proof by induction on the typing derivation.  See below.

LEMMA[typing inversion]
If C |- e:t than a rule other than 

  C |- e:t1
  C |- t1 = t2
  ------------
  C |- e:t2

concludes C |- e:t', where C |- t=t'

Proof by induction on C |- e:t, where any derivation not rooted at the t1=t2 rule
above is a base case.  (The only induction case is the t1=t2 rule above.)

LEMMA[type weakening]
If D |- t:k and D'=D,A:k then D' |- t:k
Proof by induction on D |- t:k

LEMMA[expression weakening]
If C = D;G;P;L
and C'=D,A:k;G;P;L or C'=D;G,!x->t;P;L then
(1) If C |- e:t then C' |- e:t
(2) If C |- c:t then C' |- c:t
(3a) If (C);(Cb) |- ins:t then (C');(Cb) |- ins:t
(3b) If (Ca);(C) |- ins:t then (Ca);(C') |- ins:t
(4) If C |- blk then C' |- blk
(5) If C |- n->b:t then C' |- n->b:t
(6) If C' = D';G;{};L and C |- prog then C' |- prog
Proof by inductions on typing derivations.

LEMMA[single-step type confluence]

If |- ta => tb and |- ta => tc
then there is a td s.t. |- tb=>td and |- tc => td

Proof by induction on sum of sizes of derivations of |- ta => tb and |- ta => tc.

Label the => rules as follows:

  |- t =1> t

  |- tj => tj' ... |- tk => tk'
  ------------------------------
  |- T[t1...tk] =2> T[t1'...tk']

  |- (\A:k.tb) ta =3> [A<-ta]tb

  |- rec t =4> %(t (rec t))

  |- (%t1) t2 =5> %(t1 t2)

For brevity, the cases below elide the "|- ".

The following x,y produce syntactically legal ta =x> tb and ta =y> tc:
   x,x
   1,y
   x,1
   2,y
   x,2

CASE 1,y: ta=tb, so choose td=tc

CASE x,1: ta=tc, so choose td=tb

CASE 2,2:
   T[ta1...tak] => T[tb1...tbk]
   T[ta1...tak] => T[tc1...tck]
   By induction, tb1=>td1...tbk=>tdk and tc1=>td1...tck=>tdk
   By rule =2>:
     T[tb1...tbk] => T[td1...tdk]
     T[tc1...tck] => T[td1...tdk]

CASE x,x for x=3,4,5,6: tb=tc, so choose td=tb=tc

CASE 2,3:
(\A:k.ta') ta'' => (\A:k.tb') tb'' where ta'=>tb' and ta''=>tb''
(\A:k.ta') ta'' => [A<-ta'']ta'
Choose td = [A<-tb'']tb'


CASE 2,4:
rec ta' => rec tb' where ta' => tb'
rec ta' => %(ta' (rec ta'))
choose td = %(tb' (rec tb'))


CASE 2,5:

(%ta1) ta2 => (%tb1) tb2 where ta1=>tb1 and ta2=>tb2
(%ta1) ta2 => %(ta1 ta2)
Choose td = %(tb1 tb2)


CASES 3,2 and 4,2 and 5,2 and 6,2: see cases 2,3 and 2,4 and 2,5 and 2,6


LEMMA[type confluence]

Define t0 =>* tn to mean t0=>t1=>t2=>t3...=>tn, where n>=0.
If |- tb = tc then there is a td s.t. |- tb =>* td and |- tc =>* td

Proof by single-step type confluence using standard tiling argument.
(e.g. see Pierce, "Types and Programming Languages")


LEMMA[single-step type equivalence inversion]

If |- S[t1...tn] => t' then t' = S[t1'...tn']
where |- t1=>t1' ... |- tn=>tn'

and:
  S[t1] = !t1 | s(t1) | all A:k.t1 | exists A:k.t1 | \A:k.t1 | %t1
  S[t1,t2] = t1 -o t2 | t1*t2 | Reg t1 t2 | Mem t1 t2 | Code t1 t2
(S is the same as T, but excludes (elim t1 t2 t3) and (t1 t2) and (rec t), and includes %t1)

Proof by cases of definition of => (no induction).  For example:

|- t1 => t1'
--------------
|- %t1 => %t1'
(no other derivation of %t1 => %t1' is possible)

It's important to observe that these rules are not applicable to S[t1...tn]=>t':
  |- (\A:k.tb) ta => [A<-ta]tb
  |- elim 0 tz ts => tz
  |- elim s(tm) tz ts => ts tm (elim tm tz ts)
  |- rec t => %(t (rec t))
  |- (%t1) t2 => %(t1 t2)
For example, (rec t) does not match any S[t1] or S[t1,t2].


LEMMA[type equivalence inversion]

If |- S[t1...tn] = S'[t1'...tm'] then S = S' and n=m and |- t1=t1' ... |- tn=tn'

Proof:
By lemma[type confluence], then there is some t''
such that |- S[t1...tn] =>* t'' and |- S'[t1'...tm'] =>* t''

By induction on number of => steps
and single-step type equivalence inversion lemma:
  - If t = S[t1...tn] and |- t =>* t'' then t'' = S[t1''...tn'']
    where |- t1 =>* t1'' ... |- tn =>* tn''
  - If t' = S'[t1'...tm'] and |- t' =>* t'' then t'' = S'[t1''...tm'']
    where |- t1' =>* t1'' ... |- tm' =>* tm''
So S=S' and m=n.
From |- tk =>* tk'' conclude |- tk = tk'' (repeated transitivity)
From |- tk' =>* tk'' conclude |- tk' = tk'' (repeated transitivity)
Thus conclude |- tk = tk' (symmetry, transitivity).


LEMMA[type equivalence kinds]
If C = D;G;P;L and |- C and |- t1=t2 then (D |- t1:k if and only if D |- t2:k)
Proof by induction on |- t1=t2.
Sample case: |- rec t = %(t (rec t))
  Consider "D |- t1:k implies D |- t2:k"
    Only one possible kinding derivation for rec t:
      D |- t:k->k
      ------------
      D |- rec t:k
    Given t:k->k, conclude:
                       D |- t:k->k
                       ------------
      D |- t:k->k      D |- rec t:k
      -----------------------------
      D |- t (rec t):k
      --------------------------
      D |- %(t (rec t)):k
  The "D |- t2:k implies D |- t1:k" direction is similar.


LEMMA[environment typing / expression kinds]
(1) If C = D;G;P;L and |- C and C |- e:t then D |- t:type
(2) Suppose C |- e:t by some typing rule with
premises ...C' |- e':t'....  Then |- C implies |- C'.

Proof by induction on C |- e:t.


LEMMA[type substitution]
If C,A:ka |- t:k and D |- ta:ka then D |- [A<-ta]t:k
Proof by induction on C,A:ka |- t:k.


LEMMA[type equivalence substitution]
If |- t1=t2
then |- [A<-t']t1=[A<-t']t2
Proof by induction on |- t1=t2.


LEMMA[expression type substitution]
If C = D;G;P;L and |- C and C |- ta:ka then
(1) If C,A:ka |- eb:tb
    then D;[A<-ta]G;P;L |- [A<-ta]eb:[A<-ta]tb
(2) If C,A:ka |- cb:tb
    then D;[A<-ta]G;P;L |- [A<-ta]cb:[A<-ta]tb
(3) If C,A:ka |- blk
    then D;[A<-ta]G;P;L |- [A<-ta]blk
(4) If C,A:ka |- n->b:tb
    then D;[A<-ta]G;P;L |- n->[A<-ta]b:[A<-ta]tb
(5) If C,A:ka |- prog
    then D;[A<-ta]G;P;L |- [A<-ta]prog
Proof by induction on typing derivations for eb,cb,blk,n->b,prog.


LEMMA[expression nonlinear substitution]
If |- !Ca,Cb and !Ca |- ea:ta then
(1) If Cb,!x:ta |- eb:tb
    then !Ca,Cb |- [x<-ea]eb:tb
(2) If Cb,!x:ta |- cb:tb
    then !Ca,Cb |- [x<-ea]cb:tb
(3) If Cb,!x:ta |- blk
    then !Ca,Cb |- [x<-ea]blk
(4) If Cb,!x:ta |- n->b:tb
    then !Ca,Cb |- n->[x<-ea]b:tb
(5) If Cb,!x:ta |- prog and Ca=D;G;{};L
    then !Ca,Cb |- [x<-ea]prog
Proof by induction on typing derivations for eb,cb,blk,n->b,prog.

CASE
!C,!x:ta |- x:ta
!Ca |- [x<-ea]x:ta
By weakening, !Cb,!Ca |- [x<-ea]x:ta

CASE
!Cb,!x:ta |- e:t
------------------
!Cb,!x:ta |- !e:!t
By induction, !Ca,!Cb |- [x<-ea]e:t
By rule, !Ca,!Cb |- !([x<-ea]e):!t
!([x<-ea]e) = [x<-ea](!e)

OTHER CASES SIMILAR


LEMMA[expression linear substitution]
If |- Ca,Cb and Ca |- ea:ta then
(1) If Cb,x:ta |- eb:tb
    then Ca,Cb |- [x<-ea]eb:tb
(2) If Cb,x:ta |- cb:tb
    then Ca,Cb |- [x<-ea]cb:tb
(3) If Cb,x:ta |- blk
    then Ca,Cb |- [x<-ea]blk
(4) If Cb,x:ta |- prog and Ca=D;G;{};L
    then Ca,Cb |- [x<-ea]prog
Proof by induction on typing derivations for eb,cb,blk,n->b,prog.

CASE
!Cb,x:ta |- x:ta
Ca |- [x<-ea]x:ta
By weakening, !Cb,Ca |- [x<-ea]x:ta

CASE
!Cb,!x:ta |- e:t
------------------
!Cb,!x:ta |- !e:!t
Case does not apply, because !x:ta does not match assumption x:ta.

OTHER CASES SIMILAR


LEMMA[pattern substitution]

If |- Ca,Cb
and |- pat:ta => D;G
and Ca |- ea:ta
and pat<-ea => [s]
then
(1) If Cb D;G |- eb:tb
    and Ca,Cb |- tb:type
    then Ca,Cb |- [s]eb:tb
(2) If Cb D;G |- cb:tb
    and Ca,Cb |- tb:type
    then Ca,Cb |- [s]cb:tb
(3) If Cb D;G |- blk
    then Ca,Cb |- [s]blk
(4) If Cb D;G |- n->b:tb
    and Ca,Cb |- tb:type
    then Ca,Cb |- n->[s]b:tb
(5) If Cb D;G |- prog and Ca=D;G;{};L
    then Ca,Cb |- [s]prog


By induction on pat.  Only eb cases are shown below.

CASE
pat = x
|- x:ta => {};{x:ta}
x<-ea => [x<-ea]

|- Ca,Cb
Ca |- ea:ta
Cb,x:ta |- eb:tb
By lemma[expression linear substitution], Ca,Cb |- [x<-ea]eb:tb


CASE
pat = !x
|- !x:!ta => {};{!x:ta}
!x<-!ea => [x<-ea]

Ca |- !ea:!ta
By typing inversion and type equivalence inversion:
!Ca' |- ea:ta' where !C |- ta=ta'
---------------
!Ca' |- !ea:!ta
Thus Ca=!Ca' and !Ca' |- ea:ta.

|- !Ca',Cb
!Ca' |- ea:ta
Cb,!x:ta |- eb:tb
By lemma[expression nonlinear substitution], Ca,Cb |- [x<-ea]eb:tb


CASE
pat = A,pat1
Alpha-rename so that A does not appear in Ca,Cb.

|- pat1:t' => D;G
---------------------------------
|- A,pat1:exists A:k.t' => D,A:k;G

pat1<-e1 => [s]
------------------------------------
A,pat1<-pack t,e1 as exists A:k.t'' => [A<-t][s]

Ca |- pack t,e1 as exists A:k.t'' : exists A:k.t'
By typing inversion:
  Ca |- t:k
  Ca |- e1:[A<-t]t''
  ---------------------------------
  Ca |- pack t,e1 as exists A:k.t'' : exists A:k.t''
where Ca |- exists A:k.t' = exists A:k.t''
By type equivalence inversion, Ca |- t' = t''
By type equivalence substitution, Ca |- [A<-t]t' = [A<-t]t''
So Ca |- e1:[A<-t]t'

|- pat1:t' => D;G implies |- pat1:[A<-t]t' => D;[A<-t]G (easy induction)

We know Cb D,A:k;G |- eb:tb.
Substitution implies Cb D;[A<-t]G |- [A<-t]eb:[A<-t]tb.
Since Ca,Cb |- tb:type and A does not appear in Ca,Cb, A does
not appear free in tb and [A<-t]tb = tb.

Therefore we know:
      |- Ca,Cb
  and |- pat1:[A<-t]t' => D;[A<-t]G
  and Ca |- e1:[A<-t]t'
  and Cb D;[A<-t]G |- [A<-t]eb:tb
  and Ca,Cb |- tb:type
  and pat1<-e1 => [s]
so by induction:
  then Ca,Cb |- [s][A<-t]eb:tb


CASE
pat = pat1,pat2

|- pat1:t1 => D1;G1
|- pat2:t2 => D2;G2
---------------------------------
|- pat1,pat2:t1*t2 => D1 D2;G1 G2

pat1<-e1 => [s1]
pat2<-e2 => [s2]
---------------------------
pat1,pat2<-e1,e2 => [s1][s2]

ta = t1*t2
ea = e1,e2

By typing inversion, type equivalence inversion:
  C1 |- e1:t1' where C1,C2 |- t1=t1'
  C2 |- e2:t2' where C1,C2 |- t2=t2'
  --------------------
  C1,C2 |- e1,e2:t1*t2
Thus C1 |- e1:t1 and C2 |- e2:t2 and Ca=C1,C2.
Cb D;G = Cb D1 D2;G1 G2 = (Cb D2;G2) D1;G1
By induction, C2,Cb D2;G2 |- [s1]eb:tb
By induction, C1,C2,Cb |- [s2][s1]eb:tb

OTHER CASES SIMILAR


THEOREM[preservation]
(1) If |- C and C |- e:t and e --> e'
    then C |- e':t

CASE
!C |- e:t
-----------
!C |- !e:!t
  where
e-->e'
--------
!e-->!e'

By induction, !C |- e':t
By rule, !C |- !e':!t

CASE
C |- e:t
C |- t = t'
-----------
C |- e:t'
where e-->e'
By induction, C |- e':t
By rule, C |- e':t'

CASE
C1 |- ef:ta -o tb
C2 |- ea:ta
-----------------
C1,C2 |- ef ea:tb
  where
ea --> ea'
----------------
ef ea --> ef ea'
C2 = D;G2;P;L2
G=G1,G2
L=L1,L2
|- C2
By induction, C2 |- ea':ta
By rule, C1,C2 |- ef ea':tb

CASE
C1 |- ef:ta -o tb
C2 |- ea:ta
-----------------
C1,C2 |- ef ea:tb
  where ef=(\pat:ta'.eb) and
pat<-ea => [s]
--------------------------
(\pat:ta'.eb) ea --> [s]eb

By typing inversion and type equality inversion:
|- pat:ta' => D;G
C1 D;G |- e:tb'
C1 |- ta' -o tb':type
------------------------------
C1 |- (\pat:ta'.eb):ta' -o tb' where C1 |- ta=ta' and C1 |- tb=tb'
By rule,  C2 |- ea:ta'
So we know:
      |- C1,C2
  and |- pat:ta' => D;G
  and C2 |- ea:ta'
  and C1 D;G |- e:tb'
  and C1,C2 |- ta' -o tb':type (which implies C1,C2 |- tb':type)
  and pat<-ea => [s]
By pattern substitution, C1,C2 |- [s]e:tb'
By rule, C1,C2 |- [s]e:tb

CASE
Cf |- ef:%(ta -o tb)
Ca |- ea:%ta
------------------------
Cf,Ca |- ef %<< ea : %tb
  where
ea --> ea'
------------------------
ef %<< ea --> ef %<< ea'
Cf = D;Gf;P;Lf
Ca = D;Ga;P;La
G=Ga,Gb
L=La,Lb
|- Ca
By induction, and Ca |- ea':%ta
By rule, C |- ef %<< ea' : %tb

CASE
Cf |- %ef:%(ta -o tb)
Ca |- %ea:%ta
-------------------------
Cf,Ca |- %ef %<< %ea : %tb
  where
%ef %<< %ea --> %(ef ea)
C=Cf,Ca

By typing inversion and type equivalence inversion:
Ca |- ea:ta' where Ca |- ta=ta'
--------------
Ca |- %ea:%ta'
By rule, Ca |- ea:ta

By typing inversion and type equivalence inversion:
Cf |- ef:tab' where Cf |- %(ta -o tb)=tab'
--------------
Cf |- %ef:%tab'
By rule, Ca |- ef:ta -o tb

Cf |- ef:ta -o tb
Ca |- ea:ta
-------------------
Ca,Cf |- ef ea : tb
-----------------------
Ca,Cf |- %(ef ea) : %tb

OTHER CASES SIMILAR

THEOREM[preservation]
(2) If C = D;G;P;L and |- C and C |- c:t
    and c --> c'
    then C |- c':t
(note: case c=e handled by (1))

CASE
C |- c:%t
---------
C |- #c:t
  where
c --> c'
----------
#c --> #c'
By induction:
    C |- c':%t
By rule, C |- #c':t

CASE
C |- %e:%t
-----------
C |- #%e:t
  where
#%e --> e
By typing inversion:
C |- e:t'
-----------
C |- %e:%t' where C |- %t=%t'
By type equivalence inversion, C |- t=t'
By rule, C |- e:t


THEOREM[preservation]
(3) If C = D;G;P;Lp and |- C,Ls and C |- prog
    and Ls,Lp;prog --> L';prog'
    then |- C',Ls and C' |- prog'
    where C' = D;G;P;Lp' and L'=Ls,Lp' for some Lp'
(note: prog = B blk is covered by (6))

CASE
prog = (B [c]jmp m)

C1 |- c:(Code m t') * t'
------------------------
C1 |- [c]jmp m
!C1 |- n1->b1:t1' ... !C1 |- nn->bn:tn'
--------------------------------------------
D;G;{};Lp |- B [c]jmp m

  where B = {n1->b1,...,nn->bn}
  where C1 = D;G;{n1->t1',...,nn->tn');Lp
  where c = (code(n)[t1...tj],v) and L=Ls,Lp and:

pat<-v => [s]
------------------------------------------------------------------------
B |- L;[c]jmp m --> L;[s][Aj<-tj]...[A1<-t1]blk
-------------------------------------------------------------------------
(L;B [c]jmp m) --> L;B [s][Aj<-tj]...[A1<-t1]blk
  where bm = \A1:k1...\An:kj.\pat:t.blk

Let Lp'=L.

C1 |- (code(n)[t1...tj],v):(Code m t') * t'
By typing inversion and type equivalence inversion:
C1 |- v:t'
!C1 |- code(m)[t1...tj]:Code m [Aj<-tj]...[A1<-t1]t''
  where !C1 |- t1:k1 ... !C1 |- tj:kj
  and !C1 |- t' = [A1<-t1,...,An<-tj]t''
  and !C1 |- tm' = all A1:k1...all An:kn.Code n t''

!C1 |- m->\A1:k1...\An:kj.\pat:t.blk : tm'
By inversion:
!C1,A1:k1...An:kj |- m->\pat:t.blk : tm''
  where tm' = all A1:k1...all An:kj.tm''
By inversion:
|- pat:t => D1;G1
!C1,A1:k1...An:kj D1;G1 |- blk
where tm'' = Code m t
By substitution:
!C1 D1;[Aj<-tj]...[A1<-t1]G1 |- [Aj<-tj]...[A1<-t1]blk

tm' = all A1:k1...all An:kj.Code m t
!C1 |- tm' = all A1:k1...all An:kn.Code n t''
By type equivalence inversion, !C1 |- t = t''

!C1 |- t' = [Aj<-tj]...[A1<-t1]t''
By type equivalence substitution:
!C1 |- t' = [Aj<-tj]...[A1<-t1]t

|- pat:[Aj<-tj]...[A1<-t1]t => D1;[Aj<-tj]...[A1<-t1]G1
C1 |- v:[Aj<-tj]...[A1<-t1]t
pat<-v => [s]
!C1 D1;[Aj<-tj]...[A1<-t1]G1 |- [Aj<-tj]...[A1<-t1]blk
By pattern substitution:
C1 |- [s][Aj<-tj]...[A1<-t1]blk

D;G;{};Lp |- B [s][Aj<-tj]...[A1<-t1]blk


CASE
prog = (B let pat = [c1|c2]add r1<-r2+m in blk)

Cr |- fact:Reg r1 t1
Ca,Cr |-* fact:Reg r2 t2
-------------------------------------------------------
(Ca,Cr);(Cr) |- [fact|fact]add r1<-r2+m : Reg r1 (t2+m)
-------------------------------------------------------
|- pat:Reg r1 (t2+m) => D;G
Ca D;G |- blk
----------------------------------------------
C1 |- let pat = [fact|fact]add r1<-r2+m in blk
!C1 |- n1->b1:t1 ... !C1 |- nn->bn:tn
------------------------------------------------------------------------------
D;G;{};Lp |- {n1->b1,...,nn->bn} let pat = [fact|fact]add r1<-r2+m in blk

  where C1 = D;G;{n1->t1,...,nn->tn);Lp
  and C1 = Ca,Cr
  and:

Ls,Lp;[fact|fact]add r1<-r2+m --> L0,r1->L(r2)+m;fact
------------------------------------------------------------------------------------------------------------
B |- Ls,Lp;let pat = [fact|fact]add r1<-r2+m in blk --> L0,r1->L(r2)+m;let pat = fact in blk
---------------------------------------------------------------------------------------------------------------
(Ls,Lp;B let pat = [fact|fact]add r1<-r2+m in blk) --> (L0,r1->L(r2)+m;B let pat = fact in blk)
  where L = L0,r1->m0 and L = Ls,Lp

By typing inversion and type equivalence inversion:
!_Cr,r1->m1 |- fact:Reg r1 t1 where |- t1=m1 and Cr=!_Cr,r1->m1
_Car,r2->m2 |- fact:Reg r2 t2 where |- t2=m2 and Ca,Cr=_Car,r2->m2
Lp(r1) = m1
Lp(r2) = m2
L0 = Ls,Lp0

Let Lp' = Lp0,r1->L(r2)+m
|- C',Ls
Lp'(r1) = L(r2)+m = Lp(r2)+m = m2+m
Let Cr'=!_Cr,r1->m2+m
Cr' |- fact:Reg r1 (m2+m)
Cr' |- fact:Reg r1 (t2+m)
C' |- B let pat = fact in blk


OTHER CASES SIMILAR

LEMMA[canonical forms]
If C |- v:t then:
(1) If C |- t=!t' then v = !v'
(2) If C |- t=ta -o tb then v = \pat:t'.e and C |- t'=ta
(3) If C |- t=t1*t2 then v = v1,v2
(4) If C |- t=all A:k.t1 then v = \A:k.e
(5) If C |- t=exists A:k.t1 then v = pack t',v' as t'' and C |- t''=exists A:k.t1
(6) If C |- t=%t' then v = %e
(7) If C |- t=Reg t1 t2 or C |- t=Mem t1 t2 then v = fact
(8) If C |- t=Code t1 t2 then v = code(n)[t1'...tn']

Proof by induction on C |- v:t

CASE
C |- v:t'
C |- t' = t
-----------
C |- v:t
By induction, (1)...(8) hold.
(note: this is the only induction case; all other C |- v:t are base cases)

CASE
C |- e:t''
------------
C |- %e:%t''
Only case (6) applies: C |- %t''=t=%t'
Type equivalence inversion rules out other cases.
For example, C |- %t''=t=!t' violates type equivalence inversion.
So v = %e.

OTHER CASES SIMILAR

THEOREM[progress]
(1) If C = {};{};P;L and |- C and C |- e:t and e is not a value
    then there is some e' such that e --> e'

CASE
C |- e:t''
C |- t'' = t
-----------
C |- e:t
By induction, there is some e' such that e --> e'

CASE
C1 |- ef:ta -o tb
C2 |- ea:ta
-----------------
C1,C2 |- ef ea:tb
Suppose ef is not a value:
  By induction, ef-->ef', so ef ea-->ef' ea.
Otherwise, ef is a value.
By canonical forms, ef = \pat:t'.e.
(\pat:t'.e) ea steps.

CASE
C1 |- e1:%(ta -o tb)
C2 |- e2:%ta
------------------------
C1,C2 |- e1 %<< e2 : %tb
Suppose e1 is not a value:
  By induction, e1 --> e1', so e1%<<e2 --> e1'%<<e2
Otherwise, suppose e2 is not a value:
  By induction, e2 --> e2', so e1%<<e2 --> e1%<<e2'
Otherwise, e1 and e2 are values.
By canonical forms, e1=%ef and e2=%ea.
%ef %<< %ea --> %(ef ea)

OTHER CASES SIMILAR

THEOREM[progress]
(2) If C = {};{};P;L and |- C and C |- c:t and c is not a value
    then there is some c' such that c --> c'
(note: c = e is handled by (2))

CASE
C |- c:%t
---------
C |- #c:t
Suppose c is not a value:
  By induction, c --> c', so #c --> #c'
Otherwise, c is a value.
By canonical forms, c = %e.
#%e --> e

THEOREM[progress]
(3) If C = {};{};P;Lp and |- C,Ls and C |- prog
    then there is some L';prog' such that Ls,Lp;prog --> Ls,Lp';prog'

CASE
prog = B [c]jmp m

C1 |- c:(Code m t) * t
----------------------
C1 |- [c]jmp m
!C1 |- n1->b1:t1 ... !C1 |- nn->bn:tn
-------------------------------------
D;G;{};L |- B [c]jmp m
  where C1 = D;G;{n1->t1,...,nn->tn);L
  and B = {n1->b1,...,nn->bn}
If c is not a value:
  By (3), c steps, so [c]jmp n steps by congruence.
Otherwise, c is a value.
By canonical forms, c = (code(m)[t1...tj],v) where:
  D |- t1:k1 ... D |- tj:kj
  tm = all A1:k1...all Aj:kj.Code m t'
  t = [Aj<-tj]...[A1<-t1]t'
By inversion on !C1 |- m->bm:tm :
  !C1,A1:k1,...,Aj:kj |- m->bm':Code m t'
  where bm = \A1:k1...\Aj:kj.bm'
  bm' = \pat:t'.blk

pat<-v => [s]
------------------------------------------------------------------------
B |- L;[code(n)[t1...tj],v]jmp n --> L;[s][Aj<-tj]...[A1<-t1]blk
  where bm=\A1:k1...\An:kj.\pat:t'.blk

OTHER CASES SIMILAR