The Coq mailing list

[David Pereira <dpereira AT liacc.up.pt>]

Dear all,

I am trying to do some proofs about well-founded relations over finite sets, 
and I am a bit lost.

In particular, what I need is to prove that the proper inclusion on elements 
of the powerset of a set [s] is a well-founded relation.

Do any of you know of a Coq implementation that deals with this kind of 
proofs, or any other Coq code dealign with well-founded relations on finite 
sets that I can use as documentation?

Thanks in advance.

David.