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

(Apply N_A_Deduc_ind; Unfold n_admis_sub; Unfold a_admis_sub;
 Intros).
(Rewrite -> NSAV1; Apply Implies_I; Auto).
(Rewrite <- Strengthen_Hyps_eq3; Apply H with Q0:=Q0; Auto).
(Simpl; Apply A_Admis_Weaken_Top; Auto).

(Rewrite -> NSAV2; Apply AN_Axiom; Auto).
(Apply H with Q:=Q; Auto).

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

(Apply H0 with Q:=Q0; Auto).

(Rewrite -> NSAV4; Unfold VsubstAV).
(Cut (nat_compare g i); [ Destruct 1; Intro | Auto ]).
Replace P1 with Q.
(Rewrite -> nateqb_is_eq1; Auto).

(Apply Hyps_ref_eq with i:=g j:=i h:=h; Auto).

(Rewrite -> nateqb_is_eq3; Auto; Simpl; Rewrite <- DROPN4;
 Apply A_Admis_Strengthen).
(Apply A_Axiom; Auto).

(Unfold not; Intros; Apply H2; Inversion_clear H3; Inversion_clear H4;
 Auto).
Save.

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

Cut ((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)).
(Unfold n_admis_sub; Intros c; Case c; Intros).
Exact (H h n P H1 g Q a0 H2 H3).

Exact N_admis_sub.
Save.

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

Cut ((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)).
(Unfold a_admis_sub; Intros c; Case c; Clear  c; Intros).
Exact (H0 h a P H1 g Q a0 H2 H3).

Exact N_admis_sub.
Save.

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

(Induction h; Clear  h; Intros).
Simpl.
(Elim i; Clear  i; Auto).

(Elim i; Auto).
Intros.
Simpl.
(Rewrite -> H; Auto).
Save.

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

(Intros; Apply L_Deriv_ind1; Clear  l0 h l P; Unfold n_admis_phi; Intros).
(Simpl; Apply AN_Axiom; Apply A_Axiom; Auto).

Simpl.
Rewrite <- (SW_Id h O Q).
Rewrite -> Weaken_Hyps_eq1.
(Apply N_Admis_Sub with Q:=Q; Auto).
Simpl.
(Apply Implies_E with P:=P Q:=Q; Auto).
(Apply A_Axiom; Auto).

Simpl.
(Apply Implies_I; Auto).
Save.

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

Cut (h:Hyps)(l:L)(P:F)(l0:(L_Deriv h l P))
		(n_admis_phi h l P l0).
Unfold n_admis_phi; Auto.
Exact N_Admis_Phi_1.
Save.

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

(Intros; Rewrite <- psiphiphibar; Apply M_Admis_Psi; Apply N_Admis_Phi; Auto).
Save.