test: add regression test for `Sym.simp` eta-reduction (#13416)

This PR adds a direct regression test for issue #13416. It exercises
`Std.HashMap.getElem_insert`, whose `dom` argument is a lambda closing
over pattern variables, and checks that the discrimination tree lookup
finds the theorem once the target's `dom` lambda is eta-reduced.

Closes #13416

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>