The general strategy is to define a type-preserving translation from
emf* to CiC, showing the translation to be a simulation
--------------------------------------------------------------------------------

We take this to be a definition of a fragment of CiC


    P, Q ::= x
          | Type_i
          |         |       | False
  	  | I       |       | True
          | \x:P. Q | P Q   | Pi x:P. Q
          | (P, Q)  | fst P | snd P | prod
      	  | Inl P   | Inr P | case (P as y) \x.P \x.Q returns P' | sum

  G ::= . | G, x1:P


  With the standard typing and reduction rules

    G ok
   ---------------
    G |- x : G(x)


    G ok
   ---------------
    G |- x : G(x)


   ---------------------------
    G |- Type_i : Type_{i+1}


   -------------------
    G |- False : Type0


   -------------------
    G |- True : Type0


   -------------------
    G |- I : True

    ....


    G |- e : sum Q1 Q2
    G, y:sum Q1 Q2 |- Q : Type_i
    G, x:Q1 |- P1 : Q [Inl x/y]
    G, x:Q2 |- P2 : Q [Inr x/y]
   --------------------------------------------------- [C-Case]
    G |- case (P as y) \x.P1 \x.P2 returns Q : Q[P/y]

--------------------------------------------------------------------------------

Fact (CiC is SN): G |- M : N ==> M is strongly normalizing.

--------------------------------------------------------------------------------

Translation of emf* to CiC
    _______________
   |               |
   | trans_S T = P |
   |_______________|

	With respect to a fixed signature S, and emf* term T is
	translated to a CiC term P

	Since the signature S is invariant, we leave it implicit below.

   The translation is very uniform:
       0. Erase refinement types
       1. Erase the WPs from computation types
       2. Erase reify and reflect
       3. Inline the definitions of return, bind, lift, and the actions

Following the syntax of emf* reproduced here:

           wp, t, e ::= x | a                             -- where x and a are both variables
		     |  Type_i
		     |  T
		     |  x:t{t'}
		     |  x:t -> C
		     |  fun (x:t) -> e
		     |  e1 e2
		     |  case (e as y) x.e1 y.e2 returns t -- dependent sum elimination
		     |  run e                             -- "reify" for pure terms
		     |  reify e
		     |  reflect e
		     |  M.return t e                      -- written explicitly
		     |  M.bind t1 t2 wp1 e1 wp2 x.e2
		     |  M.lift_M' t wp e
		     |  M.a ts                            -- fully applied actions
		     

   trans x      = x
   trans a      = a
   trans Type_i = Type_i
   trans unit   = True
   trans false  = False
   trans prod   = prod
   trans sum    = sum
   ... 
   translation of all remaining constants are just the identity


   trans  (x:t{t'})   = trans t //just erase the refinement
   trans  (x:t -> C)  = Pi x:trans t. transC C
   transC (Tot t)     = trans t
   transC (Pure t wp) = trans t  //just erase the WPs
   transC (F t wp)    = trans (S.unfold (F t wp))
   	     where S.unfold (F t wp) is the representation of (F t wp)
	

   trans (fun (x:t) -> e) = \x:trans t. trans e

   trans (case (e as y) x.e1 x.e2 returns t)
      = case (trans e as y) x.trans e1
      	     	      	    x.trans e2
	returns (trans t)


   trans (run e)     = trans e

   trans (reify e)   = trans e
   trans (reflect e) = trans e
   
   trans (Pure.return _ e)             = trans e
   trans (Pure.bind t1 t2 _ _ e \x.e2) = (\x:trans t1. trans e2) (trans e)

   trans (M.bind t1 t2 wp1 wp2 e1 e2)
      = (trans (S.unfold (M.bind)))
      	      (trans t1)
	      (trans t2)
	      (trans wp1)
	      (trans wp2)
	      (trans e1)
	      (transe e2)

   trans (M.return t e)
      = (trans (S.unfold (M.return)))
      	      (trans t)
	      (trans e)

   trans (M.lift_M' t wp e)
      = (trans (S.unfold (M.lift_M')))
      	      (trans t)
	      (trans wp)
	      (trans e)

   trans (M.a ts)
      = (trans (S.unfold M.a))
      	      (trans ts)

--------------------------------------------------------------------------------

Lemma 1 (Translation preserves types):
           S; G |- e : C
     ==>   trans_S G |- trans_S e : transC_s C
Proof: Easy induction on the structure of the emf* typing derivation.

We illustrate a couple of the main cases:

Case (T-Reify):
           S; G |- reify e : Tot (S.unfold (F t wp))

	   From the premise, we have:
	              S; G |- e : F t wp
		      
	   From the IH: we have

	              trans_S G |- trans_S e : trans_S (F t wp)

		    where trans_S (F t wp) = trans_S (S.unfold (F t wp))

		    which is exactly what is needed for the conclusion,
		    since trans_S (reify e) = trans_S e

Case (T-Reflect): Just the dual of T-Reify.

Case (T-Return):

       S; G |- M.return t e : M t _

       with
	  S; G |- t : Tot Type0
	  S; G |- e : Tot t

       From the IH: we have, in translated contexts
       	    trans_S t : Type_i
	    trans_S e : trans_s t

       We need to show that
       	  (S.unfold M.return) (trans_S t) (trans_S e) : trans_S (M t _)

       But, from well-formedness of S;G, we have
       	    (S.unfold M.return) : a:Type0 -> x:a -> Tot (S.unfold (M a _))

       From which the proof is nearly immediate.

Case (T-Bind): Like T-Return, but with many more arguments.
--------------------------------------------------------------------------------
Lemma 1.1 (Substitution commutes with translation)
      forall e v. trans (e[v/x]) = trans e [trans v / x]

Proof: Easy induction on e, noting that in most cases, translation is
       just homomorphic.
--------------------------------------------------------------------------------

Lemma 2 (Translation is a forward simulation):

There exists a well-founded relation >> on emf* terms such that

    forall e, e'.
            e ~> e'
    ==>     (trans e' = trans e /\ e >> e') //no steps in CiC, but decreases according to >>
    	 \/ (trans e -> trans e')           //CiC steps

Proof: 
   Pick e1 >> e2 to be:

          (one case for each Reify-* rule)

     1.         reify (reflect v) >> v     (Reify-Reflect)

     2.         run (Pure.return v) >> v   (Reify-PureRet)

     3.         reify (M.return t e)       (Reify-Ret)
	    >>  (S.unfold M.return) t e    

     4.      	run (Pure.bind t1 t2 _ _ c v) (Reify-PureBind)
     		>> run (v (run c))

     5.         reify (M.bind t1 t2 wp1 wp2 c1 \x.c2)       (Reify-Bind)
	    >>  (S.unfold M.bind)
	        (reify t1)
		(reify t2)
		(reify wp1)
		(reify wp2)
	    	(reify c1)
		(\x. reify c2)

     ...   one such case for each Reify-* rule
     
     n.    e1 >> e2 ==> E[e1] >> E[e2], for any evaluation context E.


   >> is trivially well-founded: in fact, using a well-founded
      relation here is overkill, since the relation is extremely
      simple, just relating pairs of points, without any chains to
      consider.

The proof is by induction on the transition relation e ~> e'

Case (Beta): e1 = (fun (x:t) -> e1')
     	     e2 = v
	     e' = e1'[v/x]

		      trans e1 = \x:trans t. trans e1'
		      trans e2 = trans v
		      trans e' = trans(e1'[v/x])
		      	       = trans(e1')[trans v / x] by  Lemma 1.1


case (Proj-L, Proj-R): Easy

case (Case-L, Case-R): Easy, using Lemma 1.1

case (Reify-Reflect):
     e = reify (reflect v)
     e' = v

     trans e  = trans v
     trans e' = trans v'

     Conclude using the LHS of the disjunction and case 3 of >>.

case (Reify-PureRet, Reify-PureBind, ...)
     All these cases are similar to Reify-Reflect

Case (Context):
    Broadly, using
     1. the induction hypothesis
     2. the closure of >> by emf* evaluation contexts
     3. showing that every emf* evaluation context is matched by a CiC redex

--------------------------------------------------------------------------------

Theorem: S; G |- e : C ==> e is normalizing

Proof:
 From Lemma 1: trans_S G |- trans_S e : trans_S C

 From Fact (CiC is SN): trans_S e has no infinite reduction sequence.
 
 For contradiction, suppose e has an infinite reduction sequence.

 But, from Lemma 2, every reduction sequence in emf* can be broken
 into a sequence of finite-length fragments, where each such fragment
 is matched by a single step of reduction in CiC.

 Since there are no infinite reduction sequences in CiC, e cannot have
 an infinite reduction.