The Coq mailing list

["Birgit Fruth" <birgit AT fruth.org>]

Hallo!

I try to expand the examples of Coq'Art chapter 13. So I tried to build a  
lemma which says, that a special automaton-tree fulfills a property.  
(There is already one for LLists.)
It works only for empty trees. So I think there is a type-confict with s0.  
What can I do? The lemma is called satisfies_p.

Could you please help me?
Thank you!

Birgit
--
Erstellt mit Operas revolutionärem E-Mail-Modul: http://www.opera.com/mail/

Attachment: uebung.v
Description: Binary data