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', lhs'_last_arg, wl
          in
          //if Env.debug env <| Options.Other "Rel"
          //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] t_lhs.pos)
  
negative.code:                     (rhs:term)
          : solution =
          //if Env.debug env <| Options.Other "Rel"
          //then BU.print4 "imitate_app 1:\n\tlhs=%s\n\tbs_lhs=%s\n\tt_res_lhs=%s\n\trhs=%s\n"
          //    (flex_t_to_string lhs)
          //    (Print.binders_to_string ", " bs_lhs)
          //    (Print.term_to_string t_res_lhs)
  