anchor.diff:  open FStar.Parser
   
   module Env = FStar.TypeChecker.Env
  +
  +let norm_before_encoding env t =
  +    let steps = [Env.Eager_unfolding;
  +                 Env.Simplify;
  +                 Env.Primops;
  +                 Env.AllowUnboundUniverses;
  +                 Env.EraseUniverses;
  +                 Env.Exclude Env.Zeta] in
  +    N.normalize steps env.tcenv t
   
   type prims_t = {
       mk:lident -> string -> term * int * list<decl>;
  
positive.code: 
  
  let encode_top_level_val uninterpreted env lid t quals =
      let tt = norm env t in
  //        if Env.debug env.tcenv <| Options.Other "SMTEncoding"
  //        then Printf.printf "Encoding top-level val %s : %s\Normalized to is %s\n"
  //            (Print.lid_to_string lid)
  
negative.code:       let bindings =
          List.map
            (fun lb ->
              let def = norm_before_encoding env lb.lbdef in
              let typ = norm_before_encoding env lb.lbtyp in
              {lb with lbdef=def; lbtyp=typ})
            bindings
        in
  