anchor.diff:          //            (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
  +              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
  +              let _, lhs', wl = copy_uvar u_lhs (bs_lhs@[S.null_binder t_last_arg]) t_res_lhs wl in
  +              let _, lhs'_last_arg, wl = copy_uvar u_lhs bs_lhs t_last_arg wl in
                 lhs', lhs'_last_arg, wl
           in
           //if Env.debug env <| Options.Other "Rel"
  
positive.code:              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
                     (a',i)::out_args, wl)
                   ((S.as_arg ct.result_typ)::ct.effect_args)
                   ([], wl)
  
negative.code:                   | Some univ ->
                      S.mk (Tm_type univ) None t.pos, univ
                in
                let _, u, wl = copy_uvar u_lhs (bs_lhs@bs) k wl in
                f u (Some univ), wl
             in
             match c.n with
             | Total (t, uopt) ->
  