The Coq mailing list

[Ersoy Bayramoglu <ersoy.bayramoglu AT epfl.ch>]

Hi,
I'm new to Coq, and I'm trying to mechanize the metatheory of a core  
module calculus. I'm following the approach described in the paper  
"Engineering Formal Metatheory". The type system has mutually  
inductive modules and expressions. Consider the simple lemmas:

Lemma open_te_rec_type_aux : forall e j V i U,
  i <> j ->
  open_te_rec j V e = open_te_rec i U (open_te_rec j V e) ->
  e = open_te_rec i U e.

Lemma open_tm_rec_type_aux : forall m j V i U,
  i <> j ->
  open_tm_rec j V m = open_tm_rec i U (open_tm_rec j V m) ->
  m = open_tm_rec i U m.

The first one is about opening type variables in expressions and the  
second is about opening type variables in modules. Since modules  
appear in expressions and expressions appear in modules, proving any  
of these lemmas require proving the other one first. How can i do  
these proofs in Coq? Is there a way for the lemmas to refer each  
other, or to prove them together? The Coq wiki has information on  
generating mutual induction principles which look quite heavy weight  
for this sort of thing. Because if I assume one of the lemmas, proving  
the other one is really trivial. If it's the only way, how can i use  
the induction principal generated by Scheme - or Combined Scheme - for  
these proofs?

Thanks,
ersoy