The Coq mailing list

[Thomas Th�m <thomas.thuem AT st.ovgu.de>]

Thanks for your answers. I cannot imagine how to use your ideas, when f and
g do not relate exactly identical expressions.

> For simplicity, only identical expression (lists of expressions) are in
the relation f (g).

Let me describe, how I would prove my theorem in informal math.

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? (The "Fact ... with ..." looks
pretty close to what I need, but I couldn't get it working without a=a' and
l=l'.)

Thomas