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

Recursive Definition
    Weaken_Hyps : nat->F->Hyps->Hyps :=
	O P h => (Add_Hyp P h) |
	(S n) P MT => MT |
	(S n) P (Add_Hyp Q h) => (Add_Hyp Q (Weaken_Hyps n P h)).

Lemma In_Weaken_Hyps :
	(i,j:nat)(h:Hyps)(P,Q:F)
	 (lt j (S (Len_Hyps h)))->
	  (In_Hyps i P h)->
	   (In_Hyps (lift_V j i) P (Weaken_Hyps j Q h)).

(Unfold lift_V; Intros i j; Cut (nat_compare2 i j); Auto;
 Unfold nat_compare2; Intros c; Case c; Clear  c; Intros c).
(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb; Intros h;
 Generalize i j c ; Elim h; Clear  c j i; Intros).
Inversion H0.

Simpl in H0.
(Generalize H0 H1 ; Clear  H0 H1; Inversion_clear c; Intros).
(Simpl; Inversion_clear H1; Auto; Simpl).

Simpl.
(Inversion_clear H1; Inversion_clear H2).
(Apply inhyps_rec; Apply H; Auto).

Rewrite -> ltb_is_lt3.
(Unfold Setifb;
 Case c; Clear  c; Intros c h; Generalize i j c ; Elim h; Clear  c i j;
 Intros).
Inversion H0.

(Generalize H0 H1 ; Rewrite -> c; Clear  H0 H1 c i; Intros).
Simpl in H0.
(Generalize H0 ; Clear  H0; Inversion_clear H1; Simpl; Auto; Intros).
(Apply inhyps_rec; Inversion_clear H1; Apply H; Auto).

Inversion H0.

(Generalize H0 H1 ; Clear  H0 H1; Inversion_clear c).
(Intros; Simpl; Auto).

(Simpl; Intros).
(Apply inhyps_rec; Inversion_clear H1; Inversion_clear H2; Apply H;
 Auto).

(Case c; Clear  c; Intros).
(Apply notltii; Auto).

(Apply ltnotlt; Auto).
Save.

Definition n_admis_weaken :
	(h:Hyps)(n:N)(P:F)(N_Deduc h n P)->Prop :=
	 [h:Hyps][n:N][P:F][D:(N_Deduc h n P)]
	  (j:nat)(Q:F)
	   (lt j (S (Len_Hyps h)))->
	    (N_Deduc (Weaken_Hyps j Q h) (lift_N j n) P).

Definition a_admis_weaken :
	(h:Hyps)(a:A)(P:F)(A_Deduc h a P)->Prop :=
	 [h:Hyps][a:A][P:F][D:(A_Deduc h a P)]
	  (j:nat)(Q:F)
	   (lt j (S (Len_Hyps h)))->
	    (A_Deduc (Weaken_Hyps j Q h) (lift_A j a) P).

Lemma N_admis_weaken :
	((h:Hyps)(n:N)(R:F)(n0:(N_Deduc h n R))(n_admis_weaken h n R n0))/\
	 ((h:Hyps)(a:A)(R:F)(a0:(A_Deduc h a R))(a_admis_weaken h a R a0)).

(Apply N_A_Deduc_ind; Unfold n_admis_weaken; Unfold a_admis_weaken;
 Intros).
Simpl.
(Apply Implies_I; Auto).
(Rewrite <- Weaken_Hyps_eq3; Apply H; Auto).

Rewrite -> LIFTN2.
(Apply AN_Axiom; Apply H; Auto).

(Rewrite -> LIFTN3; Apply Implies_E with P:=P1 Q:=Q).
(Apply H; Auto).

(Apply H0; Auto).

Simpl.
(Apply A_Axiom; Auto).
(Apply In_Weaken_Hyps; Auto).
Save.

Lemma N_Admis_Weaken :
	(h:Hyps)(n:N)(P:F)(j:nat)(Q:F)
	 (N_Deduc h n P)->
	   (lt j (S (Len_Hyps h)))->
	    (N_Deduc (Weaken_Hyps j Q h) (lift_N j n) P).

Cut ((h:Hyps)(n:N)(R:F)(n0:(N_Deduc h n R))(n_admis_weaken h n R n0))/\
	 ((h:Hyps)(a:A)(R:F)(a0:(A_Deduc h a R))(a_admis_weaken h a R a0)).
Unfold n_admis_weaken.
Intros c; Case c; Clear c; Intros.
Apply H; Auto.
Exact N_admis_weaken.
Save.

Lemma A_Admis_Weaken :
	(h:Hyps)(a:A)(P:F)(j:nat)(Q:F)
	 (A_Deduc h a P)->
	   (lt j (S (Len_Hyps h)))->
	    (A_Deduc (Weaken_Hyps j Q h) (lift_A j a) P).

Cut ((h:Hyps)(n:N)(R:F)(n0:(N_Deduc h n R))(n_admis_weaken h n R n0))/\
	 ((h:Hyps)(a:A)(R:F)(a0:(A_Deduc h a R))(a_admis_weaken h a R a0)).
Unfold a_admis_weaken.
Intros c; Case c; Clear c; Intros.
Apply H0; Auto.
Exact N_admis_weaken.
Save.

Definition l_admis_weaken :
	(h:Hyps)(l:L)(P:F)(L_Deriv h l P)->Prop :=
	 [h:Hyps][l:L][P:F][D:(L_Deriv h l P)]
	  (j:nat)(Q:F)
	   (lt j (S (Len_Hyps h)))->
	    (L_Deriv (Weaken_Hyps j Q h) (lift_L j l) P).

Lemma L_admis_weaken :
	(h:Hyps)(l:L)(P:F)(D:(L_Deriv h l P))
	 (l_admis_weaken h l P D).

(Intros; Apply L_Deriv_ind1; Clear  D h l P; Unfold l_admis_weaken;
 Intros; Auto).
Simpl.
(Apply L_Axiom; Apply In_Weaken_Hyps; Auto).

Simpl.
(Apply Implies_L with P:=P Q:=Q; Auto).
(Apply In_Weaken_Hyps; Auto).

Rewrite <- Weaken_Hyps_eq3.
(Apply H0; Auto).

Simpl.
(Apply Implies_R; Auto).
(Rewrite <- Weaken_Hyps_eq3; Apply H; Auto).
Save.

Lemma L_Admis_Weaken :
	(h:Hyps)(l:L)(P,Q:F)(j:nat)
	 (L_Deriv h l P)->
	  (lt j (S (Len_Hyps h)))->
	   (L_Deriv (Weaken_Hyps j Q h) (lift_L j l) P).

Intros.
Cut (h:Hyps)(l:L)(P:F)(D:(L_Deriv h l P))(l_admis_weaken h l P D).
(Unfold l_admis_weaken; Intros; Auto).

Exact L_admis_weaken.
Save.