@Armael I added the simp_all tactic. See new test for an example.
expr
level
hash_map
rb_map
has_repr
has_to_string
(t) and