I looked for places where @msammler's new tactic could be useful, and to my surprise found only two, but still.
IMO the tactic makes this clearer, but having to write the parentheses and fun H => is a bit awkward -- is there any way we could use Tactic Notation to make this look nicer?