The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Gábor Bakos wrote:
> I miss an entry regarding the cardinality related formulation. I would
> like to reason about finite sets' cardinality. Is it well supported

This is the only one of your queries that I can respond to usefully, but 
my answer is another question: What do you mean by "finite sets"?  I can 
think of at least two different meanings: the [FSets] library modules, 
or values of type [Set] that can be proved to have only finitely many 
inhabiting values.