Add a tactic for more "automatic" `notypeclasses refine`

One annoying aspect of notypeclasses refine is getting the number of underscores right. It'd be worth exploring a tactic that does this automatically: doing something like ospecialize_foralls (maybe even using that tactic), notypeclasses apply inspects the type of the argument and adds _ until it is no longer syntactically a function type, then it calls notypeclasses refine. Basically, it autoamtically adds the right number of _, at least for simple cases where the lemma is stated as ... → Q → P and is meant to apply exactly to goals matching P.