anchor.diff:                solve env (attempt [sub_prob] (solve_prob orig None [sol] wl))
   
               | (x, imp)::formals ->
  -              let ctx_u_x, u_x, wl = copy_uvar u_lhs (U.arrow bs (S.mk_Total (U.type_u() |> fst))) wl in
  -              let t_y = S.mk_Tm_app u_x bs_terms None x.sort.pos in
  +              let _ctx_u_x, u_x, wl = copy_uvar u_lhs (U.arrow (bs_lhs@bs) (S.mk_Total (U.type_u() |> fst))) wl in
  +              let t_y = S.mk_Tm_app u_x (bs_lhs_args@bs_terms) None x.sort.pos in
                 //printfn "Generated formal %s where %s" (Print.term_to_string t_y) (Print.ctx_uvar_to_string ctx_u_x);
                 let y = S.new_bv (Some (S.range_of_bv x)) t_y in
                 aux (bs@[y, imp]) (bs_terms@[S.bv_to_name y, imp]) formals wl
  
positive.code:                   | Some univ ->
                      S.mk (Tm_type univ) None t.pos, univ
                in
                let _, u, wl = copy_uvar u_lhs (U.arrow bs (S.mk_Total k)) wl in
                f (S.mk_Tm_app u bs_terms None c.pos) (Some univ), wl
             in
             match c.n with
             | Total (t, uopt) ->
  
negative.code:                     (lhs:flex_t) (bs_lhs:binders) (t_res_lhs:term)
                      (rhs:term)
          : solution =
          let bs_lhs_args = List.map (fun (x, i) -> S.bv_to_name x, i) bs_lhs in
          let rhs_hd, args = U.head_and_args rhs in
          let args_rhs, last_arg_rhs = BU.prefix args in
          let rhs' = S.mk_Tm_app rhs_hd args_rhs None rhs.pos in
          let t_lhs, u_lhs, _lhs_args = lhs in
          let lhs', lhs'_last_arg, wl =
                let _, t_last_arg, wl = copy_uvar u_lhs (fst <| U.type_u()) wl in
                //FIXME: this may be an implicit arg ... fix qualifier
                let _, u_lhs', wl = copy_uvar u_lhs (U.arrow (bs_lhs@[S.null_binder t_last_arg]) (S.mk_Total t_res_lhs)) wl in
                let lhs' = S.mk_Tm_app u_lhs' bs_lhs_args None t_lhs.pos in
                let _, u_lhs'_last_arg, wl = copy_uvar u_lhs (U.arrow bs_lhs (S.mk_Total t_last_arg)) wl in
                let lhs'_last_arg = S.mk_Tm_app u_lhs'_last_arg bs_lhs_args None t_lhs.pos in
                lhs', lhs'_last_arg, wl
          in
          let sol = [TERM(u_lhs, U.abs bs_lhs (S.mk_Tm_app lhs' [S.as_arg lhs'_last_arg] None t_lhs.pos)
  