anchor.diff:               let out_args, wl =
                  List.fold_right
                    (fun (a, i) (out_args, wl) ->
  -                   let _, t_a, wl = copy_uvar u_lhs (fst <| U.type_u()) wl in
  -                   let _, a', wl = copy_uvar u_lhs (U.arrow bs (S.mk_Total t_a)) wl in
  -                   let a' = S.mk_Tm_app a' bs_terms None a.pos in
  +                   let _, t_a, wl = copy_uvar u_lhs [] (fst <| U.type_u()) wl in
  +                   let _, a', wl = copy_uvar u_lhs bs t_a wl in
                      (a',i)::out_args, wl)
                    ((S.as_arg ct.result_typ)::ct.effect_args)
                    ([], wl)
  
positive.code:         //            (Print.args_to_string [last_arg_rhs]);
          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
          //if Env.debug env <| Options.Other "Rel"
  
negative.code:     let t = mk (Tm_uvar (ctx_uvar, ([], None))) None r in
      ctx_uvar, t, {wl with wl_implicits=(reason, t, ctx_uvar, r)::wl.wl_implicits}
  
  let copy_uvar u (bs:binders) t wl =
      let env = {wl.tcenv with gamma = u.ctx_uvar_gamma } in
      let env = Env.push_binders env bs in
      new_uvar u.ctx_uvar_reason wl u.ctx_uvar_range env.gamma
              (Env.all_binders env) t u.ctx_uvar_should_check
  
  (* --------------------------------------------------------- *)
  (* </new_uvar>                                               *)
  