anchor.diff:                let lhs'_last_arg = S.mk_Tm_app u_lhs'_last_arg bs_lhs_args None t_lhs.pos in
                 lhs', lhs'_last_arg, wl
           in
  +        //if Env.debug env <| Options.Other "RelCheck"
  +        //then printfn "imitate_app 3:\n\tlhs'=%s\n\tlast_arg_lhs=%s\n"
  +        //            (Print.term_to_string lhs')
  +        //            (Print.term_to_string lhs'_last_arg);
           let sol = [TERM(u_lhs, U.abs bs_lhs (S.mk_Tm_app lhs' [S.as_arg lhs'_last_arg] None t_lhs.pos)
                                               (Some (U.residual_tot t_res_lhs)))]
           in
  
positive.code:                     (lhs:flex_t) (bs_lhs:binders) (t_res_lhs:term)
                      (rhs:term)
          : solution =
          let bs_lhs_args = List.map (fun (x, i) -> S.bv_to_name x, i) bs_lhs in
          let rhs_hd, args = U.head_and_args rhs in
          let args_rhs, last_arg_rhs = BU.prefix args in
          let rhs' = S.mk_Tm_app rhs_hd args_rhs None rhs.pos in
          let t_lhs, u_lhs, _lhs_args = lhs in
          let lhs', lhs'_last_arg, wl =
                let _, t_last_arg, wl = copy_uvar u_lhs (fst <| U.type_u()) wl in
  
negative.code:     let rec aux pat_binders formals t_res args =
          match formals, args with
          | [], []
          |  _, [] ->
            Some (List.rev pat_binders, U.arrow formals (S.mk_Total t_res))
  
          | (formal, _)::formals, (a, _)::args ->
              begin
  