Require MinMJ_Exchange2.
Require MinMJ_Exchange3.
Require MinMJ_L_Admis_RhoBar.

Lemma Exchange_Lift_V :
	(v,x,y:V)
	 (x=y)->
	  (V_Exchange x (lift_V y v))=
	   (lift_V (S y) v).

Definition exchange_lift_m : M->Prop :=
	[m:M](x,y:V)
	 x=y->
	  (M_Exchange x (lift_M y m))=
	   (lift_M (S y) m).

Definition exchange_lift_ms : Ms->Prop :=
	[ms:Ms](x,y:V)
	 x=y->
	  (Ms_Exchange x (lift_Ms y ms))=
	   (lift_Ms (S y) ms).

Lemma Exchange_lift_m :
	((m:M)(exchange_lift_m m))/\
	 ((ms:Ms)(exchange_lift_ms ms)).

Lemma Exchange_Lift_M :
	(x,y:V)(m:M)
	 x=y->
	  (M_Exchange x (lift_M y m))=
	   (lift_M (S y) m).

Lemma Exchange_Lift_Ms :
	(x,y:V)(ms:Ms)
	 x=y->
	  (Ms_Exchange x (lift_Ms y ms))=
	   (lift_Ms (S y) ms).

Lemma Lift_Exchange_V1 :
	(v,x,y:V)
	 (lt x (S y))->
	  (lift_V x (V_Exchange y v))=
	   (V_Exchange (S y) (lift_V x v)).

Definition lift_exchange_m1 : M->Prop :=
	[m:M](x,y:nat)
	 (lt x (S y))->
	  (lift_M x (M_Exchange y m))=
	   (M_Exchange (S y) (lift_M x m)).

Definition lift_exchange_ms1 : Ms->Prop :=
	[ms:Ms](x,y:nat)
	 (lt x (S y))->
	  (lift_Ms x (Ms_Exchange y ms))=
	   (Ms_Exchange (S y) (lift_Ms x ms)).

Lemma lift_exchange_M1 :
	((m:M)(lift_exchange_m1 m))/\
	 ((ms:Ms)(lift_exchange_ms1 ms)).

Lemma Lift_Exchange_M1 :
	(m:M)(x,y:nat)
	 (lt x (S y))->
	  (lift_M x (M_Exchange y m))=
	   (M_Exchange (S y) (lift_M x m)).

Lemma Lift_Exchange_Ms1 :
	(ms:Ms)(x,y:nat)
	 (lt x (S y))->
	  (lift_Ms x (Ms_Exchange y ms))=
	   (Ms_Exchange (S y) (lift_Ms x ms)).

Definition exchange_rhobar_bridge : M->Prop :=
	[m:M](x:V)
	 (L_Exchange x (rhobar m))=
	  (rhobar (M_Exchange x m)).

Definition exchange_rhobar1_bridge : Ms->Prop :=
	[ms:Ms](x,y:V)
	 (L_Exchange x (rhobar (sc y ms)))=
	  (rhobar (M_Exchange x (sc y ms))).

Lemma Exchange_rhobar_bridge :
	((m:M)(exchange_rhobar_bridge m))/\
	 ((ms:Ms)(exchange_rhobar1_bridge ms)).

Lemma Exchange_RhoBar_Bridge :
	(x:nat)(m:M)
	 (L_Exchange x (rhobar m))=
	  (rhobar (M_Exchange x m)).

Definition height_m_exchange : M->Prop :=
	[m:M](x:nat)
	 (Height_M (M_Exchange x m))=
	  (Height_M m).

Definition height_ms_exchange : Ms->Prop :=
	[ms:Ms](x:nat)
	 (Height_Ms (Ms_Exchange x ms))=
	  (Height_Ms ms).

Lemma Height_m_exchange :
	((m:M)(height_m_exchange m))/\
	 ((ms:Ms)(height_ms_exchange ms)).

Lemma Height_M_Exchange :
	(m:M)(x:nat)
	 (Height_M (M_Exchange x m))=
	  (Height_M m).

Lemma Height_Ms_Exchange :
	(ms:Ms)(x:nat)
	 (Height_Ms (Ms_Exchange x ms))=
	  (Height_Ms ms).

Definition msub_exch_bridge1 : M->Prop :=
	[m:M](x,y:V)(m1:M)
	 (MsubstVMV x m1 y (M_Exchange y m))=
	  (MsubstVMV x m1 (S y) m).

Definition mssub_exch_bridge1 : Ms->Prop :=
	[ms:Ms](x,y:V)(m1:M)
	 (MssubstVMV x m1 y (Ms_Exchange y ms))=
	  (MssubstVMV x m1 (S y) ms).

Lemma Msub_exch_bridge1 :
	((m:M)(msub_exch_bridge1 m))/\
	 ((ms:Ms)(mssub_exch_bridge1 ms)).

Lemma Msub_Exch_Bridge1 :
	 (m:M)(x,y:V)(m1:M)
	 (MsubstVMV x m1 y (M_Exchange y m))=
	  (MsubstVMV x m1 (S y) m).

Lemma Mssub_Exch_Bridge1 :
	(ms:Ms)(x,y:V)(m1:M)
	 (MssubstVMV x m1 y (Ms_Exchange y ms))=
	  (MssubstVMV x m1 (S y) ms).