Require MinMJ_phibar.
Require MinMJ_phi.
Require MinMJ_psitheta.
Require MinMJ_thetapsi.

Definition lift_psi_bridge : N->Prop :=
[n:N](i:nat)(lift_M i (psi n)) = (psi (lift_N i n)).

Definition lift_psi'_bridge : A->Prop :=
[a:A](ms:Ms)(i:nat)(lift_M i (psi' a ms))=(psi' (lift_A i a) (lift_Ms i ms)).

Lemma Lift_psi_Bridge : 
           ((n:N)(lift_psi_bridge n))/\
           ((a:A)(lift_psi'_bridge a)).

Lemma Lift_Psi_Bridge : (n:N)(i:nat)(lift_M i (psi n)) = (psi (lift_N i n)).

Lemma Lift_Psi'_Bridge : (a:A)(ms:Ms)(i:nat)
(lift_M i (psi' a ms))=(psi' (lift_A i a) (lift_Ms i ms)).

Lemma Lift_Theta_Bridge : 
	(m:M)(i:nat)(lift_N i (theta m)) = (theta (lift_M i m)).

Lemma Lift_Theta'_Bridge : (a:A)(ms:Ms)(i:nat)
(lift_N i (theta' a ms))=(theta' (lift_A i a) (lift_Ms i ms)).

Lemma Lift_Lift_M_Bridge : 
	(m:M)(i,j:nat)
	 (lt i j)->
	  (lift_M i (lift_M j m))=
	   (lift_M (S j) (lift_M i m)).

Lemma Lift_Lift_Ms_Bridge : 
	(ms:Ms)(i,j:nat)
	 (lt i j)->
	  (lift_Ms i (lift_Ms j ms))=
	   (lift_Ms (S j) (lift_Ms i ms)).

Lemma Lift_Lift_M_Bridge0 : 
	(m:M)(i,j:nat)
	 (lt j i)->
	  (lift_M i (lift_M j m))=
	   (lift_M j (lift_M (pred i) m)).

Lemma Lift_Lift_Ms_Bridge0 : 
	(ms:Ms)(i,j:nat)
	 (lt j i)->
	  (lift_Ms i (lift_Ms j ms))=
	   (lift_Ms j (lift_Ms (pred i) ms)).

Lemma Lift_Lift_M_Bridge1 : 
	(m:M)(i,j:nat)
	 i=j->
	  (lift_M i (lift_M j m))=
	   (lift_M (S j) (lift_M i m)).

Lemma Lift_Lift_Ms_Bridge1 : 
	(ms:Ms)(i,j:nat)
	 i=j->
	  (lift_Ms i (lift_Ms j ms))=
	   (lift_Ms (S j) (lift_Ms i ms)).

Definition msub_psi_bridge : N->Prop :=
	[n2:N](n1:N)(x,y:V)
	 (MsubstVMV x (psi n1) y (psi n2))=
	  (psi (NsubstAV (ap (var x) n1) y n2)).

Definition msub_psi'_bridge : A->Prop :=
	[a:A](x:V)(n:N)(y:V)(ms:Ms)
	 (MsubstVMV x (psi n) y (psi' a ms))=
	  (psi' (AsubstAV (ap (var x) n) y a) (MssubstVMV x (psi n) y ms)).

Lemma Msub_psi_bridge : 
	((n:N)(msub_psi_bridge n))/\((a:A)(msub_psi'_bridge a)).

Lemma Msub_Psi_Bridge :
	(n2:N)(n1:N)(x,y:V)
	 (MsubstVMV x (psi n1) y (psi n2))=
	  (psi (NsubstAV (ap (var x) n1) y n2)).

Lemma Msub_Psi'_Bridge :
	(a:A)(x:V)(n:N)(y:V)(ms:Ms)
	 (MsubstVMV x (psi n) y (psi' a ms))=
	  (psi' (AsubstAV (ap (var x) n) y a) (MssubstVMV x (psi n) y ms)).

Lemma Nsub_Theta_Bridge :
	(x:V)(m1:M)(y:V)(m2:M)
	 (NsubstAV (ap (var x) (theta m1)) y (theta m2))
	  =(theta (MsubstVMV x m1 y m2)).

Definition theta_drop_m_bridge : M->Prop :=
	[m:M](i:nat)(theta (drop_M i m))=(drop_N i (theta m)).

Definition theta'_drop_ms_bridge : Ms->Prop :=
	[ms:Ms](a:A)(i:nat)
	(theta' (drop_A i a) (drop_Ms i ms))=(drop_N i (theta' a ms)).

Lemma theta_drop_M_bridge :
	((m:M)(theta_drop_m_bridge m))/\
	 ((ms:Ms)(theta'_drop_ms_bridge ms)).

Lemma Theta_Drop_M_Bridge :
	(m:M)(i:nat)(theta (drop_M i m))=(drop_N i (theta m)).

Lemma Theta'_Drop_Ms_Bridge :
	(ms:Ms)(a:A)(i:nat)
	 (theta' (drop_A i a) (drop_Ms i ms))=(drop_N i (theta' a ms)).

Lemma Psi_Drop_N_Bridge :
	(n:N)(i:nat)
	 (psi (drop_N i n))=(drop_M i (psi n)).

Lemma Psi'_Drop_A_Bridge :
	(a:A)(ms:Ms)(i:nat)
	 (psi' (drop_A i a) (drop_Ms i ms))=(drop_M i (psi' a ms)).

Lemma thetaphibarphi : (l:L)(theta (phibar l))=(phi l).

Lemma psiphiphibar : (l:L)(psi (phi l))=(phibar l).