anchor.diff:                        N.Eager_unfolding; N.EraseUniverses] env.tcenv t
   let norm env t = N.normalize [N.Beta; N.Exclude N.Zeta;  //we don't know if it will terminate, so no recursion
                                 N.Eager_unfolding; N.EraseUniverses] env.tcenv t
  +let norm_to_head_constant env t =
  +     N.normalize [N.Beta;
  +                  N.WHNF;
  +                  N.Exclude N.Zeta;
  +                  N.AllowUnboundUniverses;
  +                  N.EraseUniverses;
  +                  N.UnfoldUntil Delta_constant] env t
  +
   
   let trivial_post t : Syntax.term =
       U.abs [null_binder t]
  
positive.code:                 (* Reify the body if needed *)
                  if is_reifiable_function env'.tcenv t_norm
                  then TcUtil.reify_body env'.tcenv body
                  else if quals |> List.contains Inline_for_extraction
                  then let b = N.normalize [N.Inlining;
                                    N.Eager_unfolding;
                                    N.Exclude N.Zeta;
                                    N.PureSubtermsWithinComputations;
                                    N.Primops] env'.tcenv body in
                       (* printfn "Normalized %s to %s" *)
                       (*        (Print.term_to_string body) *)
                       (*        (Print.term_to_string b); *)
                      b
                  else body
                in
                let app = mk_app curry f ftok vars in
  
negative.code:         let ee1, decls1 = encode_term e1 env in
          let xs, e2 = SS.open_term [(x, None)] e2 in
          let x, _ = List.hd xs in
          let should_use_let =
              match ee1.tm with
              | Integer _
              | FreeV _ -> false //not worth let-binding a variable or an int
              | _ ->
                let t1 = norm_to_head_constant env.tcenv t1 in
                match (SS.compress t1).n with
                | Tm_fvar fv
                  when S.fv_eq_lid fv Const.unit_lid ->
                  //don't let-bind unit-returning terms
                  //since these are likely not free in e2 anyway
                  false
                | _ -> true
          in
          if should_use_let then
              let xsym, xtm = fresh_fvar "x" Term_sort in
              let env' = push_term_var env x xtm in
              let ee2, decls2 = encode_body e2 env' in
              let tlet = Term.mkLet' ([((xsym, Term_sort), ee1)], ee2) e2.pos in
              tlet, decls1@decls2
          else
              let env' = push_term_var env x ee1 in
              let ee2, decls2 = encode_body e2 env' in
              ee2, decls1@decls2
  
  and encode_match (e:S.term) (pats:list<S.branch>) (default_case:term) (env:env_t)
                   (encode_br:S.term -> env_t -> (term * decls_t)) : term * decls_t =
  