Require MinMJ_In.

Mutual Inductive
    N:Set :=
	lam : N->N |
	an : A->N
with
    A:Set :=
	ap : A->N->A |
	var : V->A.

Scheme N_A_ind1 := Induction for N Sort Prop
  with A_N_ind1 := Induction for A Sort Prop.

Lemma N_A_ind     
     : (P:N->Prop)
        (P0:A->Prop)
         ((n:N)(P n)->(P (lam n)))
          ->((a:A)(P0 a)->(P (an a)))
             ->((a:A)(P0 a)->(n:N)(P n)->(P0 (ap a n)))
	          ->((v:V)(P0 (var v)))
		    ->(((n:N)(P n)) /\ ((a:A)(P0 a))).