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:     match quasi_pattern env flex with
      | None -> giveup env "flex-arrow subtyping, not a quasi pattern" (TProb tp)
      | Some (flex_bs, flex_t) ->
        imitate_arrow (TProb tp) env wl flex flex_bs flex_t tp.relation this_rigid
      end
  
    | _ ->
      let u, _args = U.head_and_args this_flex in
      begin
      match (SS.compress u).n with
  
negative.code: and solve_rigid_flex_or_flex_rigid_subtyping
      (rank:int)
      (env:Env.env) (tp:tprob) (wl:worklist) : solution =
    let flip = rank = flex_rigid in
    let this_flex, this_rigid = if flip then tp.lhs, tp.rhs else tp.rhs, tp.lhs in
    begin
  