I do have a question for here rather than the issue tracker though -- what's a reasonable way to go about automating these simple minded `fset`

proofs?

hmm, isn't `fset`

MathComp stuff? Then I would look into `ssrAC`

: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrAC.v

Here it is the `fset`

from extructures. And `ssrAC`

does not provide any automation does it?

Can be interesting nonetheless indeed.

my understanding of `ssrAC`

is that you get rewriting modulo AC with the regular SSR `rewrite`

, but I could be wrong

The file you gave says:

Rewriting with AC (not modulo AC), using a small scale command.

thanks for the pointer!

Last updated: Feb 08 2023 at 22:03 UTC