Is there a way to add lemmas to `simpl`

, a la Lean's or Isabelle's `simp`

?

Would the `autorewrite`

tactic help? https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#coq:tacn.autorewrite

Modulo performance, yes. I guess it's sometimes acceptable — after all, it works (slowly) for autosubst 1

Last updated: Jan 29 2023 at 06:02 UTC