anchor.diff:          let args_rhs, last_arg_rhs = BU.prefix args in
           let rhs' = S.mk_Tm_app rhs_hd args_rhs rhs.pos in
           //if Env.debug env <| Options.Other "Rel"
  -        //then printfn "imitate_app 2:\n\trhs'=%s\n\tlast_arg_rhs=%s\n"
  +        //then BU.print2 "imitate_app 2:\n\trhs'=%s\n\tlast_arg_rhs=%s\n"
           //            (Print.term_to_string rhs')
           //            (Print.args_to_string [last_arg_rhs]);
           let (Flex (t_lhs, u_lhs, _lhs_args)) = lhs in
  
positive.code:                               (lhs:flex_t)
                                (rhs:term)
      : solution =
  
      if should_defer_flex_to_user_tac env wl lhs
      then defer_to_user_tac env orig (flex_reason lhs) wl
  
negative.code:     else giveup env msg orig
  
  and defer_to_user_tac (env:Env.env) (orig:prob) reason (wl:worklist) : solution =
    if Env.debug env <| Options.Other "Rel" then
      BU.print1 "\n\t\tDeferring %s to a tactic\n" (prob_to_string env orig);
    let wl = solve_prob orig None [] wl in
    let wl = {wl with wl_deferred_to_tac=(wl.ctr, Thunk.mkv reason, orig)::wl.wl_deferred_to_tac} in
    solve env wl
  