use implicit arguments for lemmas in coq_tactics.v

• The following discussion from !338 (merged) should be addressed:

  I was tempted to use implicit arguments instead of (some of) these underscores to make the refine more readable... does that cause problems? [@Blaisorblade]

  I have been thinking about this many times. However, we should not just do it locally here, but should do it globally for all proof mode tactics. First let's get #135 fixed and then do what you suggest. [@robbertkrebbers]