The Coq mailing list

[Frederic.Blanqui AT loria.fr]

Selon Venanzio Capretta 
<Venanzio.Capretta AT mathstat.uottawa.ca>:

>   When I define two terms by mutual corecursion, I seem to get the wrong
> reductions when doing the proofs and strange errors at the end of the proof.

i have no idea but i wonder: for mutual inductive types, coq does not generate
the correct induction principle; it must be generated by hand with the scheme
command. is there a similar problem with mutual coinductive types? is it
related to your problem?