anchor.diff:          | None -> None
           end
   
  -let split_env (bvar : bv) (e : env) : option<(env * list<bv>)> =
  +let split_env (bvar : bv) (e : env) : option<(env * bv * list<bv>)> =
       let rec aux e =
           match Env.pop_bv e with
           | None -> None
           | Some (bv', e') ->
               if S.bv_eq bvar bv'
  -            then Some (e', [])
  -            else map_opt (aux e') (fun (e'', bvs) -> (e'', bv'::bvs ))
  +            then Some (e', bv', [])
  +            else map_opt (aux e') (fun (e'', bv, bvs) -> (e'', bv, bv'::bvs ))
       in
  -    map_opt (aux e) (fun (e', bvs) -> (e', List.rev bvs))
  +    map_opt (aux e) (fun (e', bv, bvs) -> (e', bv, List.rev bvs))
   
   let push_bvs e bvs =
       List.fold_left (fun e b -> Env.push_bv e b) e bvs
   
   let subst_goal (b1 : bv) (b2 : bv) (s:list<subst_elt>) (g:goal) : option<goal> =
  -    map_opt (split_env b1 (goal_env g)) (fun (e0, bvs) ->
  +    map_opt (split_env b1 (goal_env g)) (fun (e0, b1, bvs) ->
           let s1 bv = { bv with sort = SS.subst s bv.sort } in
           let bvs = List.map s1 bvs in
           let new_env = push_bvs e0 (b2::bvs) in
  
positive.code:     let bv, _ = b in
      match split_env bv (goal_env goal) with
      | None -> fail "binder is not present in environment"
      | Some (e0, bvs) -> begin
          let steps = [Env.Reify; Env.UnfoldTac]@(N.tr_norm_steps s) in
          let sort' = normalize steps e0 bv.sort in
          let bv' = { bv with sort = sort' } in
  
negative.code:     let bv, _ = b in
      match split_env bv (goal_env goal) with
      | None -> fail "binder is not present in environment"
      | Some (e0, bv, bvs) ->
          let (ty, u) = U.type_u () in
          bind (new_uvar "binder_retype" e0 ty) (fun (t', u_t') ->
          //NS: Question ... u_t' is dropped; why?
  