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).

(Intros; Rewrite <- (psitheta m); Rewrite -> Lift_Psi_Bridge;
 Apply M_Admis_Psi; Apply N_Admis_Weaken; Auto).
(Apply N_Admis_Theta; Auto).
Save.

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).

(Induction ms; Clear  ms; Intros).
Inversion_clear H.
(Apply Meet; Auto).

Inversion_clear H0.
Rewrite -> LIFTM4.
(Apply Implies_S; Auto).
(Apply M_Admis_Weaken; Auto).
Save.

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).

Intros.
Rewrite <- Weaken_Hyps_eq1.
(Apply M_Admis_Weaken; Auto).
Save.

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).

(Induction ms; Clear  ms; Intros; Auto).
(Inversion_clear H; Apply Meet; Auto).

(Inversion_clear H0; Rewrite LIFTM4; Apply Implies_S; Auto).
(Apply M_Admis_Weaken_Top; Auto).
Save.

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).

Intros.
Rewrite <- Weaken_Hyps_eq1.
(Apply N_Admis_Weaken; Auto).
Save.

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).


Intros.
Rewrite <- Weaken_Hyps_eq1.
(Apply A_Admis_Weaken; Auto).
Save.

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).

Intros.
Rewrite <- Weaken_Hyps_eq1.
(Apply L_Admis_Weaken; Auto).
Save.