Require MinMJ_N.

Mutual Inductive
    N_Deduc : Hyps -> N -> F -> Prop :=
	Implies_I :
		(h:Hyps)(P:F)(n:N)(Q:F)
		 (N_Deduc (Add_Hyp P h) n Q)->
		  (N_Deduc h (lam n) (Impl P Q)) |
	AN_Axiom :
		(h:Hyps)(a:A)(P:F)
		 (A_Deduc h a P)->
		  (N_Deduc h (an a) P)
with
    A_Deduc : Hyps -> A -> F -> Prop :=
	Implies_E :
		(h:Hyps)(a:A)(P:F)(Q:F)(n:N)
		 (A_Deduc h a (Impl P Q))->
		  (N_Deduc h n P)->
		   (A_Deduc h (ap a n) Q) |
	A_Axiom :
		(h:Hyps)(i:V)(P:F)
		 (In_Hyps i P h)->
		  (A_Deduc h (var i) P).

Scheme N_A_Deduc_ind1 := Induction for N_Deduc Sort Prop
  with A_N_Deduc_ind1 := Induction for A_Deduc Sort Prop.

Lemma N_A_Deduc_ind
     : (P:(h:Hyps)(n:N)(f:F)(N_Deduc h n f)->Prop)
        (P0:(h:Hyps)(a:A)(f:F)(A_Deduc h a f)->Prop)
          ((h:Hyps)
           (P1:F)
            (n:N)
             (Q:F)
              (n0:(N_Deduc (Add_Hyp P1 h) n Q))
               (P (Add_Hyp P1 h) n Q n0)
                ->(P h (lam n) (Impl P1 Q) (Implies_I h P1 n Q n0)))
          ->((h:Hyps)
              (a:A)
               (P1:F)
                (a0:(A_Deduc h a P1))
                 (P0 h a P1 a0)->(P h (an a) P1 (AN_Axiom h a P1 a0)))
             ->((h:Hyps)
                 (a:A)
                  (P1,Q:F)
                   (n:N)
                    (a0:(A_Deduc h a (Impl P1 Q)))
                     (P0 h a (Impl P1 Q) a0)
                      ->(n0:(N_Deduc h n P1))
                         (P h n P1 n0)
                          ->(P0 h (ap a n) Q
                              (Implies_E h a P1 Q n a0 n0)))
                ->((h:Hyps)
                    (i:V)
                     (P1:F)
                      (i0:(In_Hyps i P1 h))
                       (P0 h (var i) P1 (A_Axiom h i P1 i0)))
                   ->((h:Hyps)(n:N)(f:F)(n0:(N_Deduc h n f))(P h n f n0))/\
		     ((h:Hyps)(a:A)(f:F)(a0:(A_Deduc h a f))(P0 h a f a0)).
Intros.
Split.
Exact (N_A_Deduc_ind1 P P0 H H0 H1 H2).

Exact (A_N_Deduc_ind1 P P0 H H0 H1 H2).
Save.