The Coq mailing list

[Dachuan Yu <dachuan.yu AT yale.edu>]

Hello,

I'm having trouble figuring out how to do simultaneous inductions on
some mutual inductive propositions that I defined.

Mutual Inductive F : Type := ...
with G : Type := ....

Mutual Inductive F_Weaken : F -> F -> Prop := ...
with G_Weaken : G -> G -> Prop := ....

The lemmas that I wanted to prove are as follows:

Lemma F_Weaken_trans : (f1,f2,f3:F)
 (F_Weaken f1 f2) -> (F_Weaken f2 f3) -> (F_Weaken f1 f3).

Lemma G_Weaken_trans : (g1,g2,g3:G)
 (G_Weaken g1 g2) -> (G_Weaken g2 g3) -> (G_Weaken g1 g3).

To prove these two lemmas, I would need to do simultaneous inductions.
My question is, how to define the inductive principles and how to apply
them?

Thanks for any help!

Dachuan