Quoting @spitters on e39ea93064e9be276300fc580e2e8387c947094b (on the unified diff, so that it sticks around even if I rebase)
> Doesn't refine do this for you ?
> There is a special [rapply] in coqorico for this.

I replied:
`refine` works, but is slower (in a totally out-of-context comparison, it slows a tactic down from 2.9s to 3.5s).  The only `rapply` I could find is at http://www.cis.upenn.edu/~bcpierce/sf/LibTactics.html#lab828.