The Coq mailing list

["Andrew Gacek" <andrew.gacek AT gmail.com>]

Hi all,

I have two mutually recursive datatypes and I am trying to prove a
theorem about them which requires using mutual induction. I hope I've
defined the induction schemes, correctly, but I still don't know how
to apply them during the proof.

Inductive term : Set :=
 | one : term
 | app : term -> term -> term
 | lam : term -> term
 | clos : term -> env -> term
 with env : Set :=
 | id : env
 | shift : env
 | cons : term -> env -> env
 | merge : env -> env -> env.

Scheme term_env_ind := Induction for term Sort Prop
 with env_term_ind := Induction for env Sort Prop.

Theorem Inverse : forall (t : Sigma.term) (e : Sigma.env),
 susp_to_sigma_term (sigma_to_susp_term t) = t /\
 susp_to_sigma_env (sigma_to_susp_env e) (sigma_to_susp_nl e) = e.

Have I stated the induction schemes correctly? Is the theorem in
proper form to apply those schemes? If so, how?

Thanks,
Andrew Gacek