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

[omelkonian]

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).

Originally posted by @WhatisRT in https://github.com/input-output-hk/formal-ledger-specifications/pull/231#pullrequestreview-1657151090