anchor.diff:      check_uvar_ctx_invariant reason r should_check gamma binders;
       let t = mk (Tm_uvar ctx_uvar) None r in
       ctx_uvar, t, {wl with wl_implicits=(reason, t, ctx_uvar, r, should_check)::wl.wl_implicits}
  +
  +let copy_uvar u t wl =
  +    new_uvar u.ctx_uvar_reason wl u.ctx_uvar_range u.ctx_uvar_gamma
  +             u.ctx_uvar_binders t u.ctx_uvar_should_check
   
   (* --------------------------------------------------------- *)
   (* </new_uvar>                                               *)
  
positive.code:       let formals, t_res = U.arrow_formals t_hd in
        aux [] formals t_res args
  
  (******************************************************************************************************)
  (* Main solving algorithm begins here *)
  (******************************************************************************************************)
  
negative.code:               aux (bs@[y, imp]) (bs_terms@[S.bv_to_name y, imp]) formals wl
           in
           aux [] [] formals wl
  
  and solve_binders (env:Env.env) (bs1:binders) (bs2:binders) (orig:prob) (wl:worklist)
                    (rhs:worklist -> binders -> Env.env -> list<subst_elt> -> (prob * worklist)) : solution =
  
     if debug env <| Options.Other "Rel"
     then BU.print3 "solve_binders\n\t%s\n%s\n\t%s\n"
                         (Print.binders_to_string ", " bs1)
                         (rel_to_string (p_rel orig))
                         (Print.binders_to_string ", " bs2);
  
     let rec aux wl scope env subst (xs:binders) (ys:binders) : either<(probs * formula), string> * worklist =
          match xs, ys with
          | [], [] ->
            let rhs_prob, wl = rhs wl scope env subst in
            if debug env <| Options.Other "Rel"
            then BU.print1 "rhs_prob = %s\n" (prob_to_string env rhs_prob);
            let formula = p_guard rhs_prob in
            Inl ([rhs_prob], formula), wl
  
          | (hd1, imp)::xs, (hd2, imp')::ys when (imp=imp') ->
             let hd1 = {hd1 with sort=Subst.subst subst hd1.sort} in //open both binders
             let hd2 = {hd2 with sort=Subst.subst subst hd2.sort} in
             let prob, wl = mk_t_problem wl scope orig hd1.sort (invert_rel <| p_rel orig) hd2.sort None "Formal parameter" in
             let hd1 = freshen_bv hd1 in
             let subst = DB(0, hd1)::SS.shift_subst 1 subst in  //extend the substitution
             let env = Env.push_bv env hd1 in
             begin
             match aux wl (scope @ [(hd1, imp)]) env subst xs ys with
             | Inl (sub_probs, phi), wl ->
               let phi =
                   U.mk_conj (p_guard prob)
                             (close_forall env [(hd1,imp)] phi) in
               if debug env <| Options.Other "Rel"
               then BU.print2 "Formula is %s\n\thd1=%s\n" (Print.term_to_string phi) (Print.bv_to_string hd1);
               Inl (prob::sub_probs, phi), wl
  
             | fail -> fail
             end
  
          | _ -> Inr "arity or argument-qualifier mismatch", wl in
  
     let scope = p_scope orig in //Env.bound_vars env |> List.map S.mk_binder in
     match aux wl scope env [] bs1 bs2 with
     | Inr msg, wl -> giveup env msg orig
     | Inl (sub_probs, phi), wl ->
       let wl = solve_prob orig (Some phi) [] wl in
       solve env (attempt sub_probs wl)
  
  and solve_t (env:Env.env) (problem:tprob) (wl:worklist) : solution =
      def_check_prob "solve_t" (TProb problem);
      solve_t' env (compress_tprob wl.tcenv problem) wl
  
  and solve_t_flex_rigid_eq env (orig:prob) wl
                                (lhs:flex_t)
                                (rhs:term)
      : solution =
  
      let binders_as_bv_set (bs:binders) =
          FStar.Util.as_set (List.map fst bs)
                            Syntax.order_bv
      in
  
      let mk_solution env (lhs:flex_t) (bs:binders) (rhs:term) =
          let (_, ctx_u, _) = lhs in
          let sol =
            match bs with
            | [] -> rhs
            | _ ->
              u_abs ctx_u.ctx_uvar_typ (sn_binders env bs) rhs
          in
          [TERM(ctx_u, sol)]
      in
  
      let try_quasi_pattern (orig:prob) (env:Env.env) (wl:worklist)
                            (lhs:flex_t) (rhs:term)
          : either<string, list<uvi>> * worklist =
          match quasi_pattern env lhs with
          | None ->
            Inl "Not a quasi-pattern", wl
  
          | Some (bs, _) ->
            let (t_lhs, ctx_u, args) = lhs in
            let uvars, occurs_ok, msg = occurs_check ctx_u rhs in
            if not occurs_ok
            then Inl ("quasi-pattern, occurs-check failed: " ^ (Option.get msg)), wl
            else let fvs_lhs = binders_as_bv_set (ctx_u.ctx_uvar_binders@bs) in
                 let fvs_rhs = Free.names rhs in
                 if not (BU.set_is_subset_of fvs_rhs fvs_lhs)
                 then Inl ("quasi-pattern, free names on the RHS are not included in the LHS"), wl
                 else Inr (mk_solution env lhs bs rhs), restrict_all_uvars ctx_u uvars wl
      in
  
      let imitate_app (orig:prob) (env:Env.env) (wl:worklist)
  