anchor.diff:      | x::xs -> x :: init xs
   
   (* TODO: these are mostly duplicated from FStar.Reflection.Basic, unify *)
  -let rec inspect (t:term) : tac<term_view> =
  +let rec inspect (t:term) : tac<term_view> = wrap_err "inspect" (
       let t = U.unascribe t in
       let t = U.un_uinst t in
       match t.n with
  
positive.code:         ret <| Tv_FVar fv
  
      | Tm_app (hd, []) ->
          failwith "inspect: empty arguments on Tm_app"
  
      | Tm_app (hd, args) ->
          // We split at the last argument, since the term_view does not
  
negative.code:         ret <| Tv_Type () 
  
      | Tm_arrow ([], k) ->
          failwith "empty binders on arrow"
  
      | Tm_arrow _ ->
          begin match U.arrow_one t with
  