anchor.diff:      let destruct_bound_function flid t_norm e
         : (S.binders    //arguments of the lambda abstraction
         * S.term        //body of the lambda abstraction
  -      * S.binders     //arguments of the function type, length of this component is equal to the first
  +      //* S.binders     //arguments of the function type, length of this component is equal to the first
         * S.comp)       //result comp
         * bool          //if set, we should generate a curried application of f
       =
  
positive.code:         let valid = mkApp("Valid", [l_not_a]) in
          let not_valid_a = mkNot <| mkApp("Valid", [a]) in
          [Util.mkAssume(mkForall (Env.get_range env) ([[l_not_a]], [aa], mkIff(not_valid_a, valid)), Some "not interpretation", "l_not-interp")] in
      // let mk_forall_interp : env -> string -> term -> decls_t = fun env for_all tt ->
      //     let aa = ("a", Term_sort) in
      //     let bb = ("b", Term_sort) in
      //     let xx = ("x", Term_sort) in
      //     let a = mkFreeV aa in
      //     let b = mkFreeV bb in
      //     let x = mkFreeV xx in
      //     let l_forall_a_b = mkApp(for_all, [a;b]) in
      //     let valid = mkApp("Valid", [l_forall_a_b]) in
      //     let valid_b_x = mkApp("Valid", [mk_ApplyTT b x]) in
      //     [Util.mkAssume(mkForall (Env.get_range env) ([[l_forall_a_b]], [aa;bb], mkIff(mkForall([[mk_HasTypeZ x a]], [xx], mkImp(mk_HasTypeZ x a, valid_b_x)), valid)),
      //                  Some "forall interpretation",
      //                  "forall-interp")] in
      // let mk_exists_interp : env -> string -> term -> decls_t = fun env for_some tt ->
      //     let aa = ("a", Term_sort) in
      //     let bb = ("b", Term_sort) in
      //     let xx = ("x", Term_sort) in
      //     let a = mkFreeV aa in
      //     let b = mkFreeV bb in
      //     let x = mkFreeV xx in
      //     let l_exists_a_b = mkApp(for_some, [a;b]) in
      //     let valid = mkApp("Valid", [l_exists_a_b]) in
      //     let valid_b_x = mkApp("Valid", [mk_ApplyTT b x]) in
      //     [Util.mkAssume(mkForall (Env.get_range env) ([[l_exists_a_b]], [aa;bb], mkIff(mkExists([[mk_HasTypeZ x a]], [xx], mkImp(mk_HasTypeZ x a, valid_b_x)), valid)),
      //                  Some "exists interpretation",
      //                  "exists-interp")] in
     let mk_range_interp : env -> string -> term -> decls_t = fun env range tt ->
          let range_ty = mkApp(range, []) in
          [Util.mkAssume(mk_HasTypeZ (mk_Range_const ()) range_ty, Some "Range_const typing", (varops.mk_unique "typing_range_const"))] in
  
negative.code:           then S.mk_Total <| reify_comp ({env.tcenv with lax = true}) c U_unknown
            else c
        in
        let subst_comp formals actuals comp =
            let subst = List.map2 (fun (x, _) (b, _) -> NT(x, S.bv_to_name b)) formals actuals in
            SS.subst_comp subst comp
        in
        let rec aux norm t_norm =
          let binders, body, lopt = U.abs_formals e in
          match binders with
  