anchor.diff:  
   let universe_of env e =
       if debug env Options.High then
  -      BU.print1 "Calling universe_of_aux with %s\n" (Print.term_to_string e);
  +      BU.print1 "Calling universe_of_aux with %s {\n" (Print.term_to_string e);
       let r = universe_of_aux env e in
       if debug env Options.High then
  -      BU.print1 "Got result from universe_of_aux = %s\n" (Print.term_to_string r);
  +      BU.print1 "Got result from universe_of_aux = %s }\n" (Print.term_to_string r);
       level_of_type env e r
   
   let tc_tparams env0 (tps:binders) : (binders * Env.env * universes) =
  
positive.code:   | Tm_unknown
    | Tm_uinst _ -> None
    | _ -> failwith ("Impossible! (" ^ (Print.tag_of_term t) ^ ")")
  
  and universeof_fastpath env t =
    bind_opt (typeof_tot_or_gtot_term_fastpath env t false) (fun k ->
      let rec aux (maybe_norm:bool) (k:typ) =
        match (SS.compress k).n with
        | Tm_type u -> Some u
        | Tm_meta (k, _) -> aux maybe_norm k
        | Tm_refine (x, _) -> aux maybe_norm x.sort
        | Tm_ascribed (k, _, _) -> aux maybe_norm k
        | _ ->
          if maybe_norm then aux false (N.unfold_whnf env k)
          else None in
      aux true k)
  
  (*
   * Precondition: G |- t : Tot _ or G |- t : GTot _
  
negative.code:   | Tm_delayed _
    | Tm_bvar _ -> failwith ("Impossible: " ^ Print.term_to_string t)
  
    (* Can't (easily) do this one efficiently, just return None *)
    | Tm_constant Const_reify
    | Tm_constant (Const_reflect _) -> None
  
    //For the following nodes, use the universe_of_aux function
    //since these are already Tot, we don't need to check the must_tot flag
    | Tm_name _
    | Tm_fvar _
    | Tm_uinst _
    | Tm_constant _
    | Tm_type _
    | Tm_arrow _ -> universe_of_aux env t |> Some
  
    | Tm_lazy i ->
      typeof_tot_or_gtot_term_fastpath env (U.unfold_lazy i) must_tot
  
    | Tm_abs(bs, body, Some ({residual_effect=eff; residual_typ=tbody})) ->  //AR: maybe keep residual univ too?
      let mk_comp =
  