The Coq mailing list

[Daniil Frumin <difrumin AT gmail.com>]

Hi, all

I was just curious about lack of facts for the Ensembles:
http://coq.inria.fr/stdlib/Coq.Sets.Ensembles.html

Surely, there are a lot of small (but useful) theorems to state about sets.

Another thing I was actually wondering about, is the possibility of
having rewrites using the Same_set as justifications.
I mean going from

Г, Same_set A B, In A x |- _

to

Г, Same_set A B, In B x |- _


I am not very familiar with Ltac to write it myself, but it does make
sense to me.

Cheers

-- Daniil