How to make automatic rewrites of hypothesis?

[Ayertienna]

We'd like to use some specific set of rewrites automatically, e.g.: notin_union + notin_singleton or Mem_app_or_eq etc, without specifying which hypotheses should be rewritten.

[Ayertienna]

One way to do this is to prepare a tactic a'la destruct which will cover all these cases. Or, even better, destruct_set which will destruct all set-like statements (notin & in mostly) and destruct_list - taking care of all the G ++ G' = nil and Mem (a::G) cases.