anchor.diff:  let mkAccuMatch (s:t) (cases: t -> t) (bs:((t -> term) -> list<branch>)) = Accu(Match (s, cases, bs), [])
   let mkAccuRec (b:letbinding) (bs:list<letbinding>) (env:list<t>) = Accu(Rec(b, bs, env), [])
   
  -// Embedding and De-embedding 
  +// Embedding and de-embedding 
   
   
   type embedding<'a> = {
  -  em : 'a -> t;
  -  un : t -> option<'a>;
  +  em  : 'a -> t;
  +  un  : t -> option<'a>;
  +  typ : t; 
   }
   
   let embed (e:embedding<'a>) (x:'a) : t = e.em x
   let unembed (e:embedding<'a>) (trm:t) : option<'a> = e.un trm
  -
  -let mk_emb em un = {em = em; un = un}
  +let type_of (e:embedding<'a>) : t = e.typ
  +
  +let mk_emb em un typ = {em = em; un = un; typ = typ}
  +
  +let lid_as_constr (l:lident) (us:list<universe>) (args:args) : t =
  +    mkConstruct (lid_as_fv l S.delta_constant (Some Data_ctor)) us args
  +
  +let lid_as_typ (l:lident) (us:list<universe>) (args:args) : t = 
  +    mkConstruct (lid_as_fv l S.delta_constant None) us args
  +
  +let as_iarg (a:t) : arg = (a, Some S.imp_tag)
  +let as_arg (a:t) : arg = (a, None)
  +    
   
   // Emdebbing at abstract types
   let e_any : embedding<t> = 
       let em = (fun a -> a) in 
       let un =  (fun t -> Some t) in 
  -    mk_emb em un
  +    mk_emb em un (lid_as_typ PC.term_lid [] [])
   
   // Emdebbing at type unit
   let e_unit : embedding<unit> = 
       let em a = Constant Unit in 
       let un t = Some () in // No runtime typecheck here 
  -    mk_emb em un
  +    mk_emb em un (lid_as_typ PC.unit_lid [] [])
   
   // Embeddind at type bool
   let e_bool : embedding<bool> = 
  
positive.code:   // NS:
    | Refinement of binder * t // VD: do we need to keep the aqual?
    // | Arrow of list binder * comp_t
  and args = list<(t * aqual)>
  //NS:
  // and comp_t =
  //   | Comp of lident * universes * args * flags
  
negative.code:       | Constant (Bool a) -> Some a
        | _ -> None
      in
      mk_emb em un (lid_as_typ PC.bool_lid [] [])
      
  // Embeddind at type char
  let e_char : embedding<char> = 
  