anchor.diff:  
   let trefl () : tac<unit> = wrap_err "trefl" <|
       bind (cur_goal ()) (fun g ->
  -    match destruct_eq (bnorm (goal_env g) (goal_type g)) with
  +    match destruct_eq (whnf (goal_env g) (goal_type g)) with
       | Some (l, r) ->
           _trefl l r
       | None ->
  
positive.code: // Beta reduce
  let normalize s e t = N.normalize_with_primitive_steps FStar.Reflection.Interpreter.reflection_primops s e t
  let bnorm e t = normalize [] e t
  
  (* Use this one for everything the user is supposed to see, EXCEPT
   * STATE DUMPS, as it does resugaring. For debug messages, just use plain
  
negative.code:     match split_env bv (goal_env goal) with
      | None -> fail "binder not found in environment"
      | Some (e0, bv, bvs) ->
      begin match destruct_eq (whnf e0 bv.sort) with
          | Some (x, e) ->
          begin match (SS.compress x).n with
             | Tm_name x ->
  