add 'notypeclasses apply' tactic

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.^^

Fixes #220