The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Umm, yes posed in this way it is of course "inconsistency" holds
"=" in coq means: x=y <=>  forall P x<=>P y (I'm right?)
So the "safe" way is following only syntactic equivalence.
(I does not know if other type of equivalence can holds without adding
extra axioms)
To run to the solution of your problem you have two possibility
(for what my limited experience tell)
To define a normalize representation for your sets, so that two equals
set "really are syntactically equals"
and use operation that preserve such representation (that is does not
define sets as inductive trees of operations)
or use your first naive inductive definition but create your own
equals definition not using the "=" concept.
Depending on what you want to do one case or the other is better.
In the worst case you could be required to follow both the ways and to
define conversion function between normalized version and operation
trees.