The Coq mailing list

["M. Scott Doerrie" <mdoerri AT cs.jhu.edu>]

I would really like to have an axiom-free method of constructing 
Ensembles from FSets.  However, I can't find any definition for 
Extensionality_Ensembles in FSetToFiniteSet in any version of the Coq 
standard library.  I believe this axiom would be derivable if creating 
FSets from UsualOrderedTypes, yet I can not locate it.  Did I miss 
something?  Is this not possible?

Scott Doerrie