The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Thomas Thüm wrote:
> Assume, we want to prove the two theorems A and B, where f and g are defined
> mutually inductive.
>
> A: forall a, exists a', f a a'
> B: forall l, exists l', g l l'
>
> First, I would prove A by assuming B using induction on a.
>
> Second, I would prove B by assuming A using induction on l.
>
> My question is, how do I do this in Coq?

I think you are looking for nested induction, as described here:
   http://adam.chlipala.net/cpdt/html/InductiveTypes.html#lab28