Tactics: more general `by-eq` that works recursively

[WhatisRT]

For reasons that I don't understand, I cannot transfer IntersectMBO/formal-ledger-specifications#234 here, so I'll just link it. For convenience, here's the original text:

One easy generalization of Tactic.ByEq that might be useful in a few places would be to take a tactic argument, and instead of unifying with refl instead try that tactic for the rhs of the pattern-lambda. The default can then be the tryConstrs tactic, which recursively applies constructors (so it'll try refl).