Require MinMJ_L.

Inductive
    L_Deriv : Hyps -> L -> F -> Prop :=
	L_Axiom :
		(h:Hyps)(i:V)(P:F)
		 (In_Hyps i P h)->
		  (L_Deriv h (vr i) P) |
	Implies_L :
		(h:Hyps)(i:V)(P:F)(Q:F)(l1:L)(l2:L)(R:F)
		 (In_Hyps i (Impl P Q) h)->
		  (L_Deriv h l1 P)->
		   (L_Deriv (Add_Hyp Q h) l2 R)->
		    (L_Deriv h (app i l1 l2) R) |
	Implies_R :
		(h:Hyps)(P:F)(l:L)(Q:F)
		 (L_Deriv (Add_Hyp P h) l Q)->
		  (L_Deriv h (lm l) (Impl P Q)).

Scheme L_Deriv_ind1 := Induction for L_Deriv Sort Prop.
(* New Induction scheme for inductive Proposition.*)