notypeclasses apply is like notypeclasses refine except that it adds sufficiently many underscores automatically, thus making it less fragile to use.
This version adds underscores until the term is not a function any more. That is less smart than apply/apply:, so maybe we should pick a different name? We could also try applying after each _, though that could be slow if unification goes wrong.
@msammler I found a case in the bitvector lib that seems like it could use the new tactic. I hope it is covered by tests, otherwise I am not sure if it still works.^^
