use new select tactic from std++
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?