anchor.diff:  *)
   let intro () : tac<binder> = wrap_err "intro" <|
       bind (cur_goal ()) (fun goal ->
  -    match U.arrow_one (bnorm (goal_env goal) (goal_type goal)) with
  +    match U.arrow_one (whnf (goal_env goal) (goal_type goal)) with
       | Some (b, c) ->
           if not (U.is_total_comp c)
           then fail "Codomain is effectful"
  
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:     log ps (fun () ->
          BU.print1 "Topdown_rewrite seems to have succeded with %s\n" (Print.term_to_string gt'));
      bind (push_goals gs) (fun _ ->
      add_goals [goal_with_type g gt']))))
  
  
  let t_pointwise (d : direction) (tau:tac<unit>) : tac<unit> = wrap_err "t_pointwise" <|
  