Require MinMJ_M.

Mutual Inductive
    M_Deriv : Hyps -> M -> F -> Prop :=
	Choose :
		(h:Hyps)(i:V)(P:F)(ms:Ms)(R:F)
		 (In_Hyps i P h)->
		  (Ms_Deriv h P ms R)->
		   (M_Deriv h (sc i ms) R) |
	Abstract :
		(h:Hyps)(P:F)(m:M)(Q:F)
		 (M_Deriv (Add_Hyp P h) m Q)->
		  (M_Deriv h (lambda m) (Impl P Q))
with
    Ms_Deriv : Hyps -> F -> Ms -> F -> Prop :=
	Meet :
		(h:Hyps)(P:F)
		 (Ms_Deriv h P mnil P) |
	Implies_S :
		(h:Hyps)(m:M)(P:F)(Q:F)(ms:Ms)(R:F)
		 (M_Deriv h m P)->
		  (Ms_Deriv h Q ms R)->
		   (Ms_Deriv h (Impl P Q) (mcons m ms) R).


Scheme M_Ms_Deriv_ind1 := Induction for M_Deriv Sort Prop
  with Ms_M_Deriv_ind1 := Induction for Ms_Deriv Sort Prop.

Lemma M_Ms_Deriv_ind :
	(P:(h:Hyps)(m:M)(f:F)(M_Deriv h m f)->Prop)
	(P0:(h:Hyps)(f:F)(m:Ms)(f0:F)(Ms_Deriv h f m f0)->Prop)
	 ((h:Hyps)(i:V)(P1:F)(ms:Ms)(R:F)
	  (i0:(In_Hyps i P1 h))
	   (m:(Ms_Deriv h P1 ms R))
	    (P0 h P1 ms R m)->
	     (P h (sc i ms) R (Choose h i P1 ms R i0 m)))->
	 ((h:Hyps)(P1:F)(m:M)(Q:F)
	  (m0:(M_Deriv (Add_Hyp P1 h) m Q))
	   (P (Add_Hyp P1 h) m Q m0)->
	    (P h (lambda m) (Impl P1 Q) (Abstract h P1 m Q m0)))->
	 ((h:Hyps)(P1:F)(P0 h P1 mnil P1 (Meet h P1)))->
	 ((h:Hyps)(m:M)(P1,Q:F)(ms:Ms)(R:F)
	  (m0:(M_Deriv h m P1))
	   (P h m P1 m0)->
	    (m1:(Ms_Deriv h Q ms R))
	     (P0 h Q ms R m1)->
	      (P0 h (Impl P1 Q) (mcons m ms) R
	        (Implies_S h m P1 Q ms R m0 m1)))->
	  ((h:Hyps)(m:M)(f:F)(m0:(M_Deriv h m f))(P h m f m0))/\
	  ((h:Hyps)(f:F)(m:Ms)(f0:F)(m0:(Ms_Deriv h f m f0))(P0 h f m f0 m0)).

Intros.
Split.
Exact (M_Ms_Deriv_ind1 P P0 H H0 H1 H2).

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