The Coq mailing list

[Noam Zeilberger <noam+ AT cs.cmu.edu>]

I was wondering if there is some sort of tutorial/FAQ for working with
mutually-(co)inductive definitions in Coq?  I'm looking for something
more than just the documentation of the Scheme command.  For example,
what is the most natural way of taking an ordinary mathematical proof
of a list of theorems by simultaneous induction, and encoding it in
the tactic language?  Has anyone done any significant amount of
theorem-proving using mutually-inductive definitions with more than
(say) three branches?

Noam