Require MinMJ_Weak.
Require MinMJ_N_Admis_Theta.
Require MinMJ_M_Admis_Psi.

Lemma M_Admis_Weaken :
	(h:Hyps)(m:M)(P:F)(j:nat)(Q:F)
	 (M_Deriv h m P)->
	  (lt j (S (Len_Hyps h)))->
	   (M_Deriv (Weaken_Hyps j Q h) (lift_M j m) P).

Lemma Ms_Admis_Weaken :
	(ms:Ms)(h:Hyps)(R:F)(P:F)(j:nat)(Q:F)
	 (Ms_Deriv h R ms P)->
	  (lt j (S (Len_Hyps h)))->
	   (Ms_Deriv (Weaken_Hyps j Q h) R (lift_Ms j ms) P).

Lemma M_Admis_Weaken_Top :
	(h:Hyps)(m:M)(P:F)
	 (M_Deriv h m P)->
	  (Q:F)(M_Deriv (Add_Hyp Q h) (lift_M O m) P).

Lemma Ms_Admis_Weaken_Top :
	(ms:Ms)(h:Hyps)(R,P:F)
	 (Ms_Deriv h R ms P)->
	  (Q:F)(Ms_Deriv (Add_Hyp Q h) R (lift_Ms O ms) P).

Lemma N_Admis_Weaken_Top :
	(h:Hyps)(n:N)(P:F)
	 (N_Deduc h n P)->
	  (Q:F)(N_Deduc (Add_Hyp Q h) (lift_N O n) P).

Lemma A_Admis_Weaken_Top :
	(h:Hyps)(a:A)(P:F)
	 (A_Deduc h a P)->
	  (Q:F)(A_Deduc (Add_Hyp Q h) (lift_A O a) P).

Lemma L_Admis_Weaken_Top :
	(h:Hyps)(l:L)(P:F)
	 (L_Deriv h l P)->
	  (Q:F)(L_Deriv (Add_Hyp Q h) (lift_L O l) P).