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 encoded_res_t, ty_pred, decls3 = 
                     let res_t = Util.compress_typ res_t in 
                     let encoded_res_t, decls = encode_typ_term res_t env' in 
                     encoded_res_t, mk_HasTypeWithFuel None vapp encoded_res_t, decls in
                let typingAx = Term.Assume(mkForall([vapp], vars, mkImp(guard, ty_pred)), Some "free var typing") in
                let g = decls1@decls2@decls3@typingAx::mk_disc_proj_axioms guard encoded_res_t vapp vars in
                g, env
  
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]
  