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)).
Apply N_A_ind.
Unfold lift_psi_bridge .
Intros.
Simpl.
Rewrite -> H.
Auto.

Unfold lift_psi'_bridge .
Unfold lift_psi_bridge .
Intros.
Rewrite -> ps2.
Rewrite -> LIFTN2.
Rewrite -> ps2.
Rewrite -> H.
Rewrite -> LIFTM3.
Auto.

Unfold lift_psi'_bridge .
Unfold lift_psi_bridge .
Intros.
Rewrite -> ps3.
Rewrite -> LIFTN3.
Rewrite -> H.
Rewrite -> LIFTM4.
Rewrite -> H0.
Auto.

Unfold lift_psi'_bridge .
Intros.
Rewrite -> ps4.
Rewrite -> LIFTM1.
Rewrite -> LIFTN4.
Rewrite -> ps4.
Auto.
Save.

Lemma Lift_Psi_Bridge : (n:N)(i:nat)(lift_M i (psi n)) = (psi (lift_N i n)).
Cut (and (n:N)(lift_psi_bridge n) (a:A)(lift_psi'_bridge a)).
Unfold lift_psi_bridge .
Intros H.
Case H.
Auto.

Apply Lift_psi_Bridge.
Save.

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)).
Cut (and (n:N)(lift_psi_bridge n) (a:A)(lift_psi'_bridge a)).
Unfold lift_psi'_bridge .
Intros H.
Case H.
Auto.

Apply Lift_psi_Bridge.
Save.

Lemma Lift_Theta_Bridge : 
	(m:M)(i:nat)(lift_N i (theta m)) = (theta (lift_M i m)).
Intros.
Rewrite <- (psitheta m).
Rewrite -> Lift_Psi_Bridge.
Rewrite -> thetapsi.
Rewrite -> thetapsi.
Auto.
Save.

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)).
Intros.
Rewrite <- (thetapsi'theta' a ms).
Rewrite -> Lift_Theta_Bridge.
Rewrite -> Lift_Psi'_Bridge.
Rewrite -> thetapsi'theta'.
Auto.
Save.

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

(Intros; Rewrite <- (psitheta m); Rewrite -> Lift_Psi_Bridge;
 Rewrite -> Lift_Psi_Bridge; Rewrite -> Lift_Lift_N_Bridge; Auto;
 Rewrite <- Lift_Psi_Bridge; Rewrite <- Lift_Psi_Bridge; Auto).
Save.

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

(Induction ms; Clear  ms; Auto; Intros; Rewrite -> LIFTM4;
 Rewrite -> LIFTM4; Rewrite -> Lift_Lift_M_Bridge;
 Auto; Rewrite -> H; Auto).
Save.

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

(Intros; Rewrite <- (psitheta m); Rewrite -> Lift_Psi_Bridge;
 Rewrite -> Lift_Psi_Bridge; Rewrite -> Lift_Lift_N_Bridge0; Auto;
 Rewrite <- Lift_Psi_Bridge; Rewrite <- Lift_Psi_Bridge; Auto).
Save.

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

(Induction ms; Clear  ms; Auto; Intros; Rewrite -> LIFTM4;
 Rewrite -> LIFTM4; Rewrite -> Lift_Lift_M_Bridge0;
 Auto; Rewrite -> H; Auto).
Save.

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

(Intros; Rewrite <- (psitheta m); Rewrite -> Lift_Psi_Bridge;
 Rewrite -> Lift_Psi_Bridge; Rewrite -> Lift_Lift_N_Bridge1; Auto;
 Rewrite <- Lift_Psi_Bridge; Rewrite <- Lift_Psi_Bridge; Auto).
Save.

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

(Induction ms; Clear  ms; Auto; Intros; Rewrite -> LIFTM4;
 Rewrite -> LIFTM4; Rewrite -> Lift_Lift_M_Bridge1;
 Auto; Rewrite -> H; Auto).
Save.

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

(Apply N_A_ind; Unfold msub_psi_bridge ; Unfold msub_psi'_bridge ;
 Intros).
(Rewrite -> ps1; Rewrite -> MSVMV2; Rewrite -> NSAV1; Rewrite -> ps1;
 Rewrite -> Lift_Psi_Bridge; Rewrite -> H; Auto).

(Rewrite -> ps2; Rewrite -> NSAV2; Rewrite -> ps2; Rewrite -> H;
 Rewrite -> MSVMV3; Auto).

(Rewrite -> ps3; Rewrite -> NSAV3; Rewrite -> ps3; Rewrite -> H;
 Rewrite -> MSVMV4; Rewrite -> H0; Auto).

(Rewrite -> NSAV4; Rewrite -> ps4; Rewrite -> MSVMV1; Unfold VsubstAV;
 Cut (nat_compare y v); [ Destruct 1; Intro | Auto ]).
(Rewrite -> nateqb_is_eq1; Auto; Rewrite -> H0; Auto).

(Rewrite -> nateqb_is_eq3; Auto).
Save.

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

Cut (and (n:N)(msub_psi_bridge n) (a:A)(msub_psi'_bridge a)).
Unfold msub_psi_bridge; Intros c; Case c; Auto.

Exact Msub_psi_bridge.
Save.

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

Cut (and (n:N)(msub_psi_bridge n) (a:A)(msub_psi'_bridge a)).
Unfold msub_psi'_bridge; Intros c; Case c; Auto.

Exact Msub_psi_bridge.
Save.

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)).
Intros.
Rewrite <- (psitheta m1).
Rewrite <- (psitheta m2).
Rewrite -> Msub_Psi_Bridge.
Rewrite -> psitheta.
Rewrite -> psitheta.
Rewrite -> thetapsi.
Auto.
Save.

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

Apply M_Ms_ind.
Unfold theta'_drop_ms_bridge .
Unfold theta_drop_m_bridge .
Intros.
Rewrite -> DROPM1.
Rewrite -> th1.
Rewrite <- DROPN4.
Rewrite -> H.
Rewrite -> th1.
Auto.

Unfold theta_drop_m_bridge .
Intros.
Rewrite -> DROPM2.
Rewrite -> th2.
Rewrite -> H.
Rewrite -> th2.
Rewrite -> DROPN1.
Auto.

Unfold theta'_drop_ms_bridge .
Auto.

Unfold theta'_drop_ms_bridge .
Unfold theta_drop_m_bridge .
Intros.
Rewrite -> DROPM4.
Rewrite -> th4.
Rewrite -> H.
Rewrite -> th4.
Rewrite <- H0.
Rewrite -> DROPN3.
Auto.
Save.

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

Cut ((m:M)(theta_drop_m_bridge m))/\
	 ((ms:Ms)(theta'_drop_ms_bridge ms)).
Unfold theta_drop_m_bridge.
Intros H.
Case H.
Auto.
Exact theta_drop_M_bridge.
Save.

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

Cut ((m:M)(theta_drop_m_bridge m))/\
	 ((ms:Ms)(theta'_drop_ms_bridge ms)).
Unfold theta'_drop_ms_bridge.
Intros H.
Case H.
Auto.
Exact theta_drop_M_bridge.
Save.

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

Intros.
Rewrite <- (thetapsi n).
Rewrite <- Theta_Drop_M_Bridge.
Rewrite -> psitheta.
Rewrite -> thetapsi.
Auto.
Save.

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)).
Intros.
Rewrite <- (psitheta'psi' ms a).
Rewrite <- Psi_Drop_N_Bridge.
Rewrite <- Theta'_Drop_Ms_Bridge.
Rewrite -> psitheta'psi'.
Auto.
Save.

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

(Induction l; Clear  l; Intros; Auto).
(Rewrite -> phibar_eq2; Rewrite -> phi_eq2).
Rewrite <- Nsub_Theta_Bridge.
(Rewrite -> H; Rewrite -> H0; Auto).

(Rewrite -> phibar_eq3; Rewrite -> phi_eq3; Rewrite -> th2;
 Rewrite -> H; Auto).
Save.

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

Intros.
Rewrite <- (psitheta (phibar l)).
Rewrite -> thetaphibarphi.
Auto.
Save.