anchor.diff:      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
  
positive.code:                     (rhs:term)
          : solution =
          //if Env.debug env <| Options.Other "Rel"
          //then printfn "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)
  
negative.code:       let (Flex (_t1, ctx_uv, args_lhs)) = lhs in
        match pat_vars env ctx_uv.ctx_uvar_binders args_lhs with
        | Some lhs_binders -> //Pattern
          if Env.debug env <| Options.Other "Rel" then
            BU.print_string "it's a pattern\n";
          let rhs = sn env rhs in
          let names_to_string fvs =
              List.map Print.bv_to_string (BU.set_elements fvs) |> String.concat ", "
          in
          let fvs1 = binders_as_bv_set (ctx_uv.ctx_uvar_binders @ lhs_binders) in
          let fvs2 = Free.names rhs in
          //if Env.debug env <| Options.Other "Rel" then
          //  BU.print4 "lhs \t= %s\n\
          //             FV(lhs) \t= %s\n\
          //             rhs \t= %s\n\
          //             FV(rhs) \t= %s\n"
          //               (flex_t_to_string lhs)
          //               (names_to_string fvs1)
          //               (Print.term_to_string rhs)
          //               (names_to_string fvs2);
          let uvars, occurs_ok, msg = occurs_check ctx_uv rhs in
          if not occurs_ok
          then giveup_or_defer env orig wl (Thunk.mkv <| "occurs-check failed: " ^ (Option.get msg))
  