Require MinMJ_Strength.
Require MinMJ_Exchange2.
Require MinMJ_Bridge2.

Definition
    n_admis_sub :
	(h:Hyps)(n:N)(P:F)(N_Deduc h n P)->Prop :=
	 [h:Hyps][n:N][P:F][D:(N_Deduc h n P)]
	  (g:nat)(Q:F)(a0:A)
	   (In_Hyps g Q h)->
	     (A_Deduc (Strengthen_Hyps g h) a0 Q)->
	      (N_Deduc (Strengthen_Hyps g h)
		       (NsubstAV a0 g n)
		       P).

Definition
    a_admis_sub :
	(h:Hyps)(a:A)(P:F)(A_Deduc h a P)->Prop :=
	 [h:Hyps][a:A][P:F][D:(A_Deduc h a P)]
	 (g:nat)(Q:F)(a0:A)
	  (In_Hyps g Q h)->
	    (A_Deduc (Strengthen_Hyps g h) a0 Q)->
	     (A_Deduc (Strengthen_Hyps g h)
		      (AsubstAV a0 g a)
		      P).

Lemma N_admis_sub :
	((h:Hyps)(n:N)(P:F)(D:(N_Deduc h n P))(n_admis_sub h n P D))/\
	 ((h:Hyps)(a:A)(P:F)(D:(A_Deduc h a P))(a_admis_sub h a P D)).

Lemma N_Admis_Sub :
	(h:Hyps)(n:N)(P:F)(Q:F)(a0:A)(g:nat)
	 (N_Deduc h n P)->
	  (In_Hyps g Q h)->
	    (A_Deduc (Strengthen_Hyps g h) a0 Q)->
	     (N_Deduc (Strengthen_Hyps g h)
		      (NsubstAV a0 g n)
		      P).

Lemma A_Admis_Sub :
	(h:Hyps)(a:A)(P:F)(Q:F)(a0:A)(g:nat)
	 (A_Deduc h a P)->

	  (In_Hyps g Q h)->
	    (A_Deduc (Strengthen_Hyps g h) a0 Q)->
	     (A_Deduc (Strengthen_Hyps g h) 
		      (AsubstAV a0 g a)
		      P).

Lemma SW_Id :
	(h:Hyps)(i:nat)(P:F)
	 (Strengthen_Hyps i (Weaken_Hyps i P h))=
	  h.

Definition n_admis_phi : (h:Hyps)(l:L)(P:F)(L_Deriv h l P)->Prop :=
[h:Hyps][l:L][P:F][l0:(L_Deriv h l P)](N_Deduc h (phi l) P).

Lemma N_Admis_Phi_1 : (h:Hyps)(l:L)(P:F)(l0:(L_Deriv h l P))
		(n_admis_phi h l P l0).

Lemma N_Admis_Phi : (h:Hyps)(l:L)(P:F)
	(L_Deriv h l P)->
	 (N_Deduc h (phi l) P).

Lemma M_Admis_PhiBar : (h:Hyps)(l:L)(P:F)
	(L_Deriv h l P)->
	 (M_Deriv h (phibar l) P).