anchor.diff:                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"
  +        //then BU.print2 "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)
  
positive.code:         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"
          //            (Print.term_to_string rhs')
          //            (Print.args_to_string [last_arg_rhs]);
          let (Flex (t_lhs, u_lhs, _lhs_args)) = lhs in
  
negative.code:     let first_order (orig:prob) (env:Env.env) (wl:worklist)
                      (lhs:flex_t) (rhs:term)
          : solution =
          if Env.debug env <| Options.Other "Rel" then
            BU.print_string "first_order\n";
          let is_app rhs =
             let _, args = U.head_and_args rhs in
             match args with
  