anchor.diff:      match split_env bv (goal_env goal) with
       | None -> fail "binder not found in environment"
       | Some (e0, bv, bvs) ->
  -    begin match destruct_eq bv.sort with
  +    begin match destruct_eq (whnf e0 bv.sort) with
           | Some (x, e) ->
           begin match (SS.compress x).n with
              | Tm_name x ->
  
positive.code:     bind (cur_goal ()) (fun goal ->
      BU.print_string "WARNING (intro_rec): calling this is known to cause normalizer loops\n";
      BU.print_string "WARNING (intro_rec): proceed at your own risk...\n";
      match U.arrow_one (bnorm (goal_env goal) (goal_type goal)) with
      | Some (b, c) ->
          if not (U.is_total_comp c)
          then fail "Codomain is effectful"
  
negative.code:     log ps (fun () ->
          BU.print1 "Pointwise 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 _trefl (l : term) (r : term) : tac<unit> =
     bind (cur_goal ()) (fun g ->
  