anchor.diff:      | _ ->
           mkAccuTyp u
   
  +let is_univ (tm : t)=
  +  match tm with 
  +  | Univ _ -> true
  +  | _ -> false
  +
   (* We are not targeting tagless normalization at this point *)
   let rec app (f:t) (x:t) (q:aqual) =
     debug (fun () -> BU.print2 "When creating app: %s applied to %s\n" (t_to_string f) (t_to_string x));
     match f with
     | Lam (f, _) -> f x
     | Accu (a, ts) -> Accu (a, (x,q)::ts)
  -  | Construct (i, us, ts) -> Construct (i, us, (x,q)::ts)
  -  | Unit
  -  | Bool _ -> failwith "Ill-typed application"
  +  | Construct (i, us, ts) ->
  +    (match x with 
  +     | Univ u -> Construct (i, u::us, ts) 
  +     | _ -> Construct (i, us, (x,q)::ts))
  +  | Unit | Bool _ | Univ _ -> failwith "Ill-typed application"
   
   and iapp (f:t) (args:list<(t * aqual)>) =
     match args with
  
positive.code: 
      | Tm_uinst (t, [u]) ->
        debug (fun () -> BU.print3 "Term with univs: %s - %s\nUniv %s\n" (P.tag_of_term t) (P.term_to_string t) (P.univ_to_string u));
        (match (SS.compress t).n with
         | Tm_fvar fv ->
            translate_fv env bs [u] fv
            // let tr = translate env bs t in
            // //t is always an fv
            // // specialize the definition of t for u (if it has one, i.e. not a constructor)
            // // don't do this here, but when looking up def of fv; if it's a constructor, just mkConstructor
            // (match tr with
            //  | Lam _ ->
            //      let x = (S.new_bv None S.tun, None) in
            //      let t' = S.mk (Tm_abs([x], t, None)) None t.pos in
            //      app (translate env bs t') (translate_univ env bs u) None
            //  | _ ->
            //      app tr (translate_univ env bs u) None)
  
         | _ -> failwith "Expected an fv")
  
      | Tm_uinst (t, _) ->
        debug (fun () -> BU.print1 "Term with univs: %s\n" (P.term_to_string t));
  
negative.code:              // let x = (S.new_bv None S.tun, None) in
               // let t' = S.mk (Tm_abs([x], t, None)) None t.pos in
               // iapp (translate env bs t') (List.map (fun u -> (translate_univ env bs u, None)) us)
               translate_letbinding env [] lb
            end
        | Some { sigel = Sig_datacon(_, _, _, lid, _, []) } ->
            debug (fun() -> BU.print1 "Translate fv %s: it's a Sig_datacon\n" (P.lid_to_string lid));
  