Require MinMJ_LJ.
Require MinMJ_MJ.
Require MinMJ_NJ.
Require MinMJ_Occurs_Lift.

Recursive Definition
    Strengthen_Hyps : nat->Hyps->Hyps :=
	n MT => MT |
	O (Add_Hyp Q h) => h |
	(S i) (Add_Hyp Q h) => (Add_Hyp Q (Strengthen_Hyps i h)).

Lemma Drop_S_Bridge_nat :
	(i,j:nat)
	 ~i=j->
	  (drop_V (S i) (S j))=
	   (S (drop_V i j)).

Lemma In_Strength :
	(h:Hyps)(i,j:nat)(P:F)
	 (In_Hyps i P h)->
	  ~i=j->
	   (In_Hyps (drop_V j i) P (Strengthen_Hyps j h)).

Definition
    n_admis_strengthen : (h:Hyps)(n:N)(Q:F)(N_Deduc h n Q)->Prop :=
	[h:Hyps][n:N][Q:F][D:(N_Deduc h n Q)]
	 (i:nat)
	  ~(Occurs_In_N i n)->
	   (N_Deduc (Strengthen_Hyps i h) (drop_N i n) Q).

Definition
    a_admis_strengthen : (h:Hyps)(a:A)(Q:F)(A_Deduc h a Q)->Prop :=
	[h:Hyps][a:A][Q:F][D:(A_Deduc h a Q)]
	 (i:nat)
	  ~(Occurs_In_A i a)->
	   (A_Deduc (Strengthen_Hyps i h) (drop_A i a) Q).

Lemma N_admis_strengthen :
	((h:Hyps)(n:N)(Q:F)(n0:(N_Deduc h n Q))
	 (n_admis_strengthen h n Q n0))/\
	 ((h:Hyps)(a:A)(Q:F)(a0:(A_Deduc h a Q))
	  (a_admis_strengthen h a Q a0)).

Lemma N_Admis_Strengthen :
	(h:Hyps)(n:N)(Q:F)(i:nat)
	 (N_Deduc h n Q)->
	  ~(Occurs_In_N i n)->
	   (N_Deduc (Strengthen_Hyps i h) (drop_N i n) Q).

Lemma A_Admis_Strengthen :
	(h:Hyps)(a:A)(Q:F)(i:nat)
	 (A_Deduc h a Q)->
	  ~(Occurs_In_A i a)->
	   (A_Deduc (Strengthen_Hyps i h) (drop_A i a) Q).

Definition l_admis_strengthen : (h:Hyps)(l:L)(Q:F)(L_Deriv h l Q)->Prop :=
	[h:Hyps][l:L][Q:F][l0:(L_Deriv h l Q)]
	 (i:nat)
	   ~(Occurs_In_L i l)->
	    (L_Deriv (Strengthen_Hyps i h) (drop_L i l) Q).

Lemma L_admis_strengthen : (h:Hyps)(l:L)(Q:F)(l0:(L_Deriv h l Q))
			(l_admis_strengthen h l Q l0).

Lemma L_Admis_Strengthen :
	(h:Hyps)(l:L)(Q:F)(i:nat)
	 (L_Deriv h l Q)->
	   ~(Occurs_In_L i l)->
	    (L_Deriv (Strengthen_Hyps i h) (drop_L i l) Q).