Require MinMJ_Exchange.

Lemma Hyps_ref_eq :
	(i,j:V)(P,Q:F)(h:Hyps)
	 i=j->
	  (In_Hyps i P h)->
	   (In_Hyps j Q h)->
	    P=Q.

Lemma V_Exch_S_Bridge :
	(i,j:nat)
	 (V_Exchange (S i) (S j))=
	  (S (V_Exchange i j)).

Lemma V_Exch_id :
	(i:nat)
	 (V_Exchange i i)=(S i).

Lemma In_Exch1 :
	(h:Hyps)(i,j:nat)(P:F)
	 (lt i j)->
	  (In_Hyps i P h)->
	   (In_Hyps i P (Hyps_Exchange j h)).

Lemma In_Exch2 :
	(h:Hyps)(i,j:nat)(P:F)
	 (lt (S j) i)->
	  (In_Hyps i P h)->
	   (In_Hyps i P (Hyps_Exchange j h)).

Lemma In_Exch :
	(i,j:nat)(h:Hyps)(P,Q,R:F)
	 (In_Hyps i P h)->
	  (In_Hyps j Q h)->
	   (In_Hyps (S j) R h)->
	    (In_Hyps (V_Exchange j i) P (Hyps_Exchange j h)).

Definition l_admis_exch1 :
	(h:Hyps)(l:L)(R:F)(L_Deriv h l R)->Prop :=
	 [h:Hyps][l:L][R:F][l0:(L_Deriv h l R)](j:nat)(P,Q:F)
	  (In_Hyps j P h)->
	   (In_Hyps (S j) Q h)->
	    (L_Deriv (Hyps_Exchange j h)
		     (L_Exchange j l)
		     R).

Lemma L_admis_exch : 
	(h:Hyps)(l:L)(R:F)(D:(L_Deriv h l R))
	 (l_admis_exch1 h l R D).

Lemma L_Admis_Exch :
	(h:Hyps)(l:L)(R:F)(j:nat)(P,Q:F)
	 (L_Deriv h l R)->
	  (In_Hyps j P h)->
	   (In_Hyps (S j) Q h)->
	    (L_Deriv (Hyps_Exchange j h)
		     (L_Exchange j l)
		     R).

Lemma Hyps_Exchange_Top :
	(P,Q:F)(h:Hyps)
	 (Hyps_Exchange O (Add_Hyp P (Add_Hyp Q h)))=
	  (Add_Hyp Q (Add_Hyp P h)).

Lemma L_Admis_Exch_Top :
	(P,Q,R:F)(h:Hyps)(l:L)
	 (L_Deriv (Add_Hyp P (Add_Hyp Q h)) l R)->
	  (L_Deriv (Add_Hyp Q (Add_Hyp P h)) (L_Exchange O l) R).

Definition n_admis_exch :
	(h:Hyps)(n:N)(R:F)(N_Deduc h n R)->Prop :=
	 [h:Hyps][n:N][R:F][n0:(N_Deduc h n R)](j:nat)(P,Q:F)
	  (In_Hyps j P h)->
	   (In_Hyps (S j) Q h)->
	    (N_Deduc (Hyps_Exchange j h)
		     (N_Exchange j n)
		     R).

Definition a_admis_exch :
	(h:Hyps)(a:A)(R:F)(A_Deduc h a R)->Prop :=
	 [h:Hyps][a:A][R:F][a0:(A_Deduc h a R)](j:nat)(P,Q:F)
	  (In_Hyps j P h)->
	   (In_Hyps (S j) Q h)->
	    (A_Deduc (Hyps_Exchange j h)
		     (A_Exchange j a)
		     R).

Lemma N_admis_exch :
	((h:Hyps)(n:N)(R:F)(n0:(N_Deduc h n R))(n_admis_exch h n R n0))/\
	 ((h:Hyps)(a:A)(R:F)(a0:(A_Deduc h a R))(a_admis_exch h a R a0)).

Lemma N_Admis_Exch : (h:Hyps)(n:N)(R:F)(j:nat)(P,Q:F)
	(N_Deduc h n R)->
	 (In_Hyps j P h)->
	  (In_Hyps (S j) Q h)->
	   (N_Deduc (Hyps_Exchange j h)
		    (N_Exchange j n)
		    R).

Lemma A_Admis_Exch : (h:Hyps)(a:A)(R:F)(j:nat)(P,Q:F)
	(A_Deduc h a R)->
	 (In_Hyps j P h)->
	  (In_Hyps (S j) Q h)->
	   (A_Deduc (Hyps_Exchange j h)
		    (A_Exchange j a)
		    R).