anchor.diff:          a_b, rest_bs, f_b, c
         | _ -> failwith "Impossible! subcomp_ty must have been an arrow with at lease 1 binder" in
   
  +    (*
  +     * An auxiliary function that we will call for then and else branches
  +     *
  +     * attr_opt is (Some arg) when there is an (ite_soundness_by arg) attribute on the effect
  +     *
  +     * The input env has the squash p (resp. squash (not p)) binder for the then (resp. else) branch
  +     *)
       let check_branch env ite_f_or_g_sort attr_opt : unit =
         let subst, uvars, g_uvars = subcomp_bs |> List.fold_left
           (fun (subst, uvars, g) b ->
            let sort = SS.subst subst b.binder_bv.sort in
            let t, _, g_t =
  +         (*
  +          * AR: TODO: now that we use fastpath for implicits checking,
  +          *           can this always be Strict?
  +          *)
            let uv_qual =
              if List.length b.binder_attrs > 0 ||
                 attr_opt |> is_some
              then Strict
              else Allow_untyped in
            let ctx_uvar_meta = BU.map_option Ctx_uvar_meta_attr attr_opt in
  -         new_implicit_var_aux "" r env sort uv_qual ctx_uvar_meta in
  +         new_implicit_var_aux
  +           (BU.format1 "uvar for subcomp %s binder when checking ite soundness"
  +             (Print.binder_to_string b))
  +           r
  +           env
  +           sort
  +           uv_qual
  +           ctx_uvar_meta in
           subst@[NT (b.binder_bv, t)], uvars@[t], conj_guard g g_t)
           ([NT (subcomp_a_b.binder_bv, S.bv_to_name a_b.binder_bv)],
            [],
  
positive.code:    * Basically when p holds, the computation type of f should be coercible to if_then_else f g
     *   and similarly for the (not p) case
     *
     * The way we program it, we first build the term:
     *   subcomp <some number of _> f <: if_then_else bs f g
     *   where bs are some variables for the extra binders of if_then_else, and f and g are also variables
     *
     * Then, we typecheck this term which fills in the _ in subcomp application and returns a guard
     * We refine the guard to add an implication p ==> guard,
     *   and then discharge it
     * 
     * Similarly for the g case
     *
     * 02/16/2021: We expect the `_` that we apply to subcomp to be instantiated
     *             by the unifier
     *
     *             However, in some cases, the binders that correspond to these `_`
     *             may be unconstrained, and hence we may fail in solving them
     *
     *             As an escape hatch, these binders can be decorated with
     *             the ite_soundness_forall attribute, in which case, instead of `_`,
     *             we use fresh names, essentially saying forall values of these
     *             binders, the proof should work
     *)
    let _if_then_else_is_sound = Errors.with_ctx "While checking if-then-else soundness" (fun () ->
      let r = (ed |> U.get_layered_if_then_else_combinator |> must |> snd).pos in
  
negative.code:       ignore (check_branch env g_b.binder_bv.sort ite_soundness_tac_attr) in
  
      ()
    )  //Errors.with_ctx
    in
  
  
  