anchor.diff:                  let tok_typing, decls2 = 
                       let env = {env with encode_non_total_function_typ=encode_non_total_function_typ} in
                       if not(head_normal env tt) 
  -                    then encode_typ_pred' None tt env vtok_tm 
  -                    else encode_typ_pred' None t_norm env vtok_tm in //NS:Unfortunately, this is duplicated work --- we effectively encode the function type twice
  +                    then encode_typ_pred None tt env vtok_tm 
  +                    else encode_typ_pred None t_norm env vtok_tm in //NS:Unfortunately, this is duplicated work --- we effectively encode the function type twice
                   let tok_typing = Term.Assume(tok_typing, Some "function token typing") in
                   let tok_decl, env = match formals with 
                           | [] -> decls2@[tok_typing], push_free_var env lid vname (Some <| mkFreeV(vname, Term_sort))
  
positive.code:             let t1 = Normalize.norm_typ [Normalize.DeltaHard; Normalize.Beta; Normalize.Eta; Normalize.EtaArgs; Normalize.Simplify] env.tcenv t0 in
              if Tc.Env.debug env.tcenv <| Options.Other "Encoding"
              then (Util.fprint3 "Normalized %s : %s to %s\n" (Print.strBvd x) (Print.typ_to_string t0) (Print.typ_to_string t1));
              let t, decls' = encode_typ_pred' None t1 env xx in
              let caption = 
                  if !Options.logQueries 
                  then Some (Util.format3 "%s : %s (%s)" (Print.strBvd x) (Print.typ_to_string t0) (Print.typ_to_string t1))
  
negative.code:                   let formals, rest = Util.first_N (List.length args_e) formals in
                    let subst = Util.formals_for_actuals formals args_e in
                    let ty = mk_Typ_fun(rest, c) (Some ktype) e0.pos |> Util.subst_typ subst in
                    let has_type, decls'' = encode_typ_pred None ty env app_tm in
                    let cvars = Term.free_variables has_type in
                    let e_typing = Term.Assume(Term.mkForall([has_type], cvars, has_type), None) in
                    app_tm, decls@decls'@decls''@[e_typing]
  