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
.