Require MinMJ_In.

Mutual Inductive
    M:Set :=
	sc : V->Ms->M |
	lambda : M->M
with
    Ms:Set :=
	mnil : Ms |
	mcons : M->Ms->Ms.

Scheme M_Ms_ind1 := Induction for M Sort Prop
  with Ms_M_ind1 := Induction for Ms Sort Prop.

(* We now join these two schemes together into the simultaneous 
induction scheme we actually want. *)

Lemma M_Ms_ind
     : (P:M->Prop)
        (P0:Ms->Prop)
         ((v:V)(m:Ms)(P0 m)->(P (sc v m)))
          ->((m:M)(P m)->(P (lambda m)))
             ->(P0 mnil)
                ->((m:M)(P m)->(m0:Ms)(P0 m0)->(P0 (mcons m m0)))
                  ->(((m:M)(P m)) /\ ((ms:Ms)(P0 ms))).

Intros; Split; Intros.
Exact (M_Ms_ind1 P P0 H H0 H1 H2 m).
Exact (Ms_M_ind1 P P0 H H0 H1 H2 ms).
Save.