Rename `simplify_eq` to avoid shadowing Coq's tactic, or document it
Then the tactic should be renamed to avoid confusion for people that are familiar with the Coq tactic.
That'd suggest renaming std++'s
simplify_eq. In fact, that seems pretty annoying, so maybe we should just prepend a comment to the definition:
(** Unrelated to Coq's own [simplify_eq]. *)