Require MinMJ_Bridge.

Lemma OI_Lift_V1_1: 
	(x:V)(i,j:nat)
	 (lt i j)->
	  (Occurs_In_V1 i (lift_V j x))=(Occurs_In_V1 i x).

Lemma OI_Lift_V1_2:
	(x:V)(i,j:nat)
	 i=j->
	  (Occurs_In_V1 i (lift_V j x))=false.

Lemma OI_Lift_V1_3 :
	(x:V)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_V1 (S i) (lift_V j x))=
	   (Occurs_In_V1 i x).

Lemma OI_Lift_V1_4 : (x:V)(i,j:nat)
	(lt j i)->
	 (Occurs_In_V1 i (lift_V j x))=
	  (Occurs_In_V1 (pred i) x).

Definition oi_lift_m1_1: M->Prop :=
	[m:M](i,j:nat)
	 (lt i j)->(Occurs_In_M1 i (lift_M j m))=(Occurs_In_M1 i m).

Definition oi_lift_ms1_1: Ms->Prop :=
	[ms:Ms](i,j:nat)
	 (lt i j)->
	  (Occurs_In_Ms1 i (lift_Ms j ms))=(Occurs_In_Ms1 i ms).

Lemma oi_lift_M1_1 :
	((m:M)(oi_lift_m1_1 m))/\
	 ((ms:Ms)(oi_lift_ms1_1 ms)).

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

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

Definition oi_lift_m1_2: M->Prop :=
	[m:M](i,j:nat)
	 i=j->(Occurs_In_M1 i (lift_M j m))=false.

Definition oi_lift_ms1_2: Ms->Prop :=
	[ms:Ms](i,j:nat)
	 i=j->(Occurs_In_Ms1 i (lift_Ms j ms))=false.

Lemma oi_lift_M1_2 :
	((m:M)(oi_lift_m1_2 m))/\
	 ((ms:Ms)(oi_lift_ms1_2 ms)).

Lemma OI_Lift_M1_2:
	(m:M)(i,j:nat)
	 i=j->
	  (Occurs_In_M1 i (lift_M j m))=false.

Lemma OI_Lift_Ms1_2:
	(ms:Ms)(i,j:nat)
	 i=j->
	  (Occurs_In_Ms1 i (lift_Ms j ms))=false.

Definition oi_lift_m1_3: M->Prop :=
	[m:M](i,j:nat)
	 (lt j i)->
	  (Occurs_In_M1 (S i) (lift_M j m))=(Occurs_In_M1 i m).

Definition oi_lift_ms1_3: Ms->Prop :=
	[ms:Ms](i,j:nat)
	 (lt j i)->
	  (Occurs_In_Ms1 (S i) (lift_Ms j ms))=(Occurs_In_Ms1 i ms).

Lemma oi_lift_M1_3 :
	((m:M)(oi_lift_m1_3 m))/\
	 ((ms:Ms)(oi_lift_ms1_3 ms)).

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

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

Definition oi_lift_m1_4: M->Prop :=
	[m:M](i,j:nat)
	 (lt j i)->
	  (Occurs_In_M1 i (lift_M j m))=(Occurs_In_M1 (pred i) m).

Definition oi_lift_ms1_4: Ms->Prop :=
	[ms:Ms](i,j:nat)
	 (lt j i)->
	  (Occurs_In_Ms1 i (lift_Ms j ms))=
	   (Occurs_In_Ms1 (pred i) ms).

Lemma oi_lift_M1_4 :
	((m:M)(oi_lift_m1_4 m))/\
	 ((ms:Ms)(oi_lift_ms1_4 ms)).

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

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

Definition oi_lift_n1_1: N->Prop :=
	[n:N](i,j:nat)
	 (lt i j)->(Occurs_In_N1 i (lift_N j n))=(Occurs_In_N1 i n).

Definition oi_lift_a1_1: A->Prop :=
	[a:A](i,j:nat)
	 (lt i j)->(Occurs_In_A1 i (lift_A j a))=(Occurs_In_A1 i a).

Lemma oi_lift_N1_1 :
	((n:N)(oi_lift_n1_1 n))/\
	 ((a:A)(oi_lift_a1_1 a)).

Lemma OI_Lift_N1_1:
	(n:N)(i,j:nat)
	 (lt i j)->
	  (Occurs_In_N1 i (lift_N j n))=(Occurs_In_N1 i n).

Lemma OI_Lift_A1_1:
	(a:A)(i,j:nat)
	 (lt i j)->
	  (Occurs_In_A1 i (lift_A j a))=(Occurs_In_A1 i a).

Definition oi_lift_n1_2 : N->Prop :=
	[n:N](i,j:nat)
	 i=j->(Occurs_In_N1 i (lift_N j n))=false.

Definition oi_lift_a1_2 : A->Prop :=
	[a:A](i,j:nat)
	 i=j->(Occurs_In_A1 i (lift_A j a))=false.

Lemma oi_lift_N1_2 :
	((n:N)(oi_lift_n1_2 n))/\
	 ((a:A)(oi_lift_a1_2 a)).

Lemma OI_Lift_N1_2:
	(n:N)(i,j:nat)
	 i=j->
	  (Occurs_In_N1 i (lift_N j n))=false.

Lemma OI_Lift_A1_2:
	(a:A)(i,j:nat)
	 i=j->
	  (Occurs_In_A1 i (lift_A j a))=false.

Definition oi_lift_n1_3: N->Prop :=
	[n:N](i,j:nat)
	 (lt j i)->
	  (Occurs_In_N1 (S i) (lift_N j n))=(Occurs_In_N1 i n).

Definition oi_lift_a1_3: A->Prop :=
	[a:A](i,j:nat)
	 (lt j i)->
	  (Occurs_In_A1 (S i) (lift_A j a))=(Occurs_In_A1 i a).

Lemma oi_lift_N1_3 : 
	((n:N)(oi_lift_n1_3 n))/\
	 ((a:A)(oi_lift_a1_3 a)).

Lemma OI_Lift_N1_3 :
	(n:N)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_N1 (S i) (lift_N j n))=(Occurs_In_N1 i n).

Lemma OI_Lift_A1_3 :	
	(a:A)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_A1 (S i) (lift_A j a))=(Occurs_In_A1 i a).

Definition oi_lift_n1_4: N->Prop :=
	[n:N](i,j:nat)
	 (lt j i)->
	  (Occurs_In_N1 i (lift_N j n))=(Occurs_In_N1 (pred i) n).

Definition oi_lift_a1_4: A->Prop :=
	[a:A](i,j:nat)
	 (lt j i)->
	  (Occurs_In_A1 i (lift_A j a))=(Occurs_In_A1 (pred i) a).

Lemma oi_lift_N1_4 : 
	((n:N)(oi_lift_n1_4 n))/\
	 ((a:A)(oi_lift_a1_4 a)).

Lemma OI_Lift_N1_4 :
	(n:N)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_N1 i (lift_N j n))=(Occurs_In_N1 (pred i) n).

Lemma OI_Lift_A1_4 :
	(a:A)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_A1 i (lift_A j a))=(Occurs_In_A1 (pred i) a).

Lemma OI_Lift_L1_4 :
	(l:L)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_L1 i (lift_L j l))=
	   (Occurs_In_L1 (pred i) l).

Definition noi_msub_b_bridge : M->Prop :=
	[m:M](x:V)(m1:M)(i:nat)
	 ~(Occurs_In_M i m)->
	  (MsubstVMV x m1 i m)=(drop_M i m).

Definition noi_mssub_b_bridge : Ms->Prop :=
	[ms:Ms](x:V)(m1:M)(i:nat)
	 ~(Occurs_In_Ms i ms)->
	  (MssubstVMV x m1 i ms)=(drop_Ms i ms).

Lemma noi_msub_b_Bridge :
	((m:M)(noi_msub_b_bridge m))/\
	 ((ms:Ms)(noi_mssub_b_bridge ms)).

Lemma NOI_Msub_Bridge :
	(m:M)(x:V)(m1:M)(i:nat)
	 ~(Occurs_In_M i m)->
	  (MsubstVMV x m1 i m)=(drop_M i m).

Lemma NOI_Mssub_Bridge :
	(ms:Ms)(x:V)(m1:M)(i:nat)
	 ~(Occurs_In_Ms i ms)->
	  (MssubstVMV x m1 i ms)=(drop_Ms i ms).

Lemma Lift_Drop_V_Bridge1 : (x:V)(i,j:nat)
	(lt j i)->
	 ~(Occurs_In_V j x)->
	  (lift_V i (drop_V j x))=
	   (drop_V j (lift_V (S i) x)).

Definition lift_drop_n_bridge1 : N->Prop :=
	[n:N](i,j:nat)
	 (lt j i)->
	  ~(Occurs_In_N j n)->
	   (lift_N i (drop_N j n))=
	    (drop_N j (lift_N (S i) n)).

Definition lift_drop_a_bridge1 : A->Prop :=
	[a:A](i,j:nat)
	 (lt j i)->
	  ~(Occurs_In_A j a)->
	   (lift_A i (drop_A j a))=
	    (drop_A j (lift_A (S i) a)).

Lemma lift_drop_n_Bridge1 :
	((n:N)(lift_drop_n_bridge1 n))/\((a:A)(lift_drop_a_bridge1 a)).

Lemma Lift_Drop_N_Bridge1 :
	(n:N)(i,j:nat)
	 (lt j i)->
	  ~(Occurs_In_N j n)->
	   (lift_N i (drop_N j n))=
	    (drop_N j (lift_N (S i) n)).

Lemma Lift_Drop_A_Bridge1 :
	(a:A)(i,j:nat)
	 (lt j i)->
	  ~(Occurs_In_A j a)->
	   (lift_A i (drop_A j a))=
	    (drop_A j (lift_A (S i) a)).

Lemma Drop_Lift_V_Bridge1 :
	(x:V)(i,j:nat)
	 ~(Occurs_In_V i x)->
	  (lt j (S i))->
	   (drop_V (S i) (lift_V j x))=
	    (lift_V j (drop_V i x)).

Definition drop_lift_n_bridge1 : N->Prop :=
	[n:N](i,j:nat)
	 ~(Occurs_In_N i n)->
	  (lt j (S i))->
	   (drop_N (S i) (lift_N j n))=
	    (lift_N j (drop_N i n)).

Definition drop_lift_a_bridge1 : A->Prop :=
	[a:A](i,j:nat)
	 ~(Occurs_In_A i a)->
	  (lt j (S i))->
	   (drop_A (S i) (lift_A j a))=
	    (lift_A j (drop_A i a)).

Lemma drop_lift_n_Bridge1 :
	((n:N)(drop_lift_n_bridge1 n))/\
	 ((a:A)(drop_lift_a_bridge1 a)).

Lemma Drop_Lift_N_Bridge1 :
	(n:N)(i,j:nat)
	 ~(Occurs_In_N i n)->
	  (lt j (S i))->
	   (drop_N (S i) (lift_N j n))=
	    (lift_N j (drop_N i n)).

Lemma Drop_Lift_A_Bridge1 :
	(a:A)(i,j:nat)
	 ~(Occurs_In_A i a)->
	  (lt j (S i))->
	   (drop_A (S i) (lift_A j a))=
	    (lift_A j (drop_A i a)).

Lemma Lift_Vsub_Bridge0 : 
	(x:V)(i,j:nat)(a:A)
	 (lt i j)->
	  (lift_A j (VsubstAV a i x))=
	   (VsubstAV (lift_A j a) i (lift_V (S j) x)).

Definition lift_nsub_b_bridge0 : N->Prop :=
	[n:N](i,j:nat)(a:A)
	 (lt i j)->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) i (lift_N (S j) n)).

Definition lift_asub_b_bridge0 : A->Prop :=
	[a:A](i,j:nat)(a1:A)
	 (lt i j)->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) i (lift_A (S j) a)).

Lemma lift_nsub_b_Bridge0 :
	((n:N)(lift_nsub_b_bridge0 n))/\ ((a:A)(lift_asub_b_bridge0 a)).

Lemma Lift_Nsub_Bridge0 :
	(n:N)(i,j:nat)(a:A)
	 (lt i j)->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) i (lift_N (S j) n)).

Lemma Lift_Asub_Bridge0 :
	(a:A)(i,j:nat)(a1:A)
	 (lt i j)->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) i (lift_A (S j) a)).

Lemma Lift_Msub_Bridge0 :
	(x:V)(m,m0:M)(i,j:nat)
	 (lt i j)->
	  (lift_M j (MsubstVMV x m i m0))=
	   (MsubstVMV (lift_V j x) (lift_M j m) i (lift_M (S j) m0)).

Lemma Lift_Mssub_Bridge0 :
	(x:V)(m:M)(ms:Ms)(i,j:nat)
	 (lt i j)->
	  (lift_Ms j (MssubstVMV x m i ms))=
	   (MssubstVMV (lift_V j x) (lift_M j m) i (lift_Ms (S j) ms)).

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

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

Lemma Lift_msub_bridge2 :
	((m:M)(lift_msub_bridge2 m))/\
	 ((ms:Ms)(lift_mssub_bridge2 ms)).

Lemma Lift_Msub_Bridge2 :
	(x:V)(m1:M)(y:V)(m:M)
	 (MsubstVMV x m1 (S y) (lift_M y (lift_M (S y) m)))=
	  (MsubstVMV x m1 y (lift_M (S (S y)) (lift_M (S y) m))).

Lemma Lift_Mssub_Bridge2 :
	(x:V)(m1:M)(y:V)(ms:Ms)
	 (MssubstVMV x m1 (S y) (lift_Ms y (lift_Ms (S y) ms)))=
	  (MssubstVMV x m1 y (lift_Ms (S (S y)) (lift_Ms (S y) ms))).

Lemma Lift_Vsub_Bridge1 : 
	(x:V)(i,j:nat)(a:A)
	 i=j->
	  (lift_A j (VsubstAV a i x))=
	   (VsubstAV (lift_A j a) i (lift_V (S j) x)).

Lemma Lift_Vsub_Bridge2 : 
	(x:V)(i,j:nat)(a:A)
	 (lt j i)->
	  (lift_A j (VsubstAV a i x))=
	   (VsubstAV (lift_A j a) (S i) (lift_V j x)).

Definition lift_nsub_b_bridge1 : N->Prop :=
	[n:N](i,j:nat)(a:A)
	 i=j->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) i (lift_N (S j) n)).

Definition lift_asub_b_bridge1 : A->Prop :=
	[a:A](i,j:nat)(a1:A)
	 i=j->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) i (lift_A (S j) a)).

Lemma lift_nsub_b_Bridge1 :
	((n:N)(lift_nsub_b_bridge1 n))/\ ((a:A)(lift_asub_b_bridge1 a)).

Lemma Lift_Nsub_Bridge1 :
	(n:N)(i,j:nat)(a:A)
	 i=j->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) i (lift_N (S j) n)).

Lemma Lift_Asub_Bridge1 :
	(a:A)(i,j:nat)(a1:A)
	 i=j->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) i (lift_A (S j) a)).

Definition lift_nsub_b_bridge2 : N->Prop :=
	[n:N](i,j:nat)(a:A)
	 (lt j i)->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) (S i) (lift_N j n)).

Definition lift_asub_b_bridge2 : A->Prop :=
	[a:A](i,j:nat)(a1:A)
	 (lt j i)->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) (S i) (lift_A j a)).

Lemma lift_nsub_b_Bridge2 :
	((n:N)(lift_nsub_b_bridge2 n))/\ ((a:A)(lift_asub_b_bridge2 a)).

Lemma Lift_Nsub_Bridge2 :
	(n:N)(i,j:nat)(a:A)
	 (lt j i)->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) (S i) (lift_N j n)).

Lemma Lift_Asub_Bridge2 :
	(a:A)(i,j:nat)(a1:A)
	 (lt j i)->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) (S i) (lift_A j a)).

Lemma Lift_Vsub_Bridge3 : 
	(x:V)(i,j:nat)(a:A)
	 i=j->
	  (lift_A j (VsubstAV a i x))=
	   (VsubstAV (lift_A j a) (S i) (lift_V j x)).

Definition lift_nsub_b_bridge3 : N->Prop :=
	[n:N](i,j:nat)(a:A)
	 i=j->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) (S i) (lift_N j n)).

Definition lift_asub_b_bridge3 : A->Prop :=
	[a:A](i,j:nat)(a1:A)
	 i=j->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) (S i) (lift_A j a)).

Lemma lift_nsub_b_Bridge3 :
	((n:N)(lift_nsub_b_bridge3 n))/\ ((a:A)(lift_asub_b_bridge3 a)).

Lemma Lift_Nsub_Bridge3 :
	(n:N)(i,j:nat)(a:A)
	 i=j->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) (S i) (lift_N j n)).

Lemma Lift_Asub_Bridge3 :
	(a:A)(i,j:nat)(a1:A)
	 i=j->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) (S i) (lift_A j a)).

Lemma Lift_Msub_Bridge1 :
	(x:V)(m,m0:M)(i,j:nat)
	 i=j->
	  (lift_M j (MsubstVMV x m i m0))=
	   (MsubstVMV (lift_V j x) (lift_M j m) i (lift_M (S j) m0)).

Lemma Lift_Mssub_Bridge1 :
	(x:V)(m:M)(ms:Ms)(i,j:nat)
	 i=j->
	  (lift_Ms j (MssubstVMV x m i ms))=
	   (MssubstVMV (lift_V j x) (lift_M j m) i (lift_Ms (S j) ms)).

Lemma Lift_Phi_Bridge : 
	(l:L)(i:nat)
	 (lift_N i (phi l))=
	  (phi (lift_L i l)).

Lemma Lift_PhiBar_Bridge :
	(l:L)(i:nat)
	 (lift_M i (phibar l))=
	  (phibar (lift_L i l)).

Lemma Drop_Lift_L :
	(l:L)(x:V)
	 (drop_L x (lift_L x l))=l.

Definition oi_theta : M->Prop :=
	[m:M](x:V)
	 (Occurs_In_M x m)->
	  (Occurs_In_N x (theta m)).

Definition oi_theta' : Ms->Prop :=
	[ms:Ms](a:A)(x:V)
	 ((Occurs_In_Ms x ms)\/(Occurs_In_A x a))->
	  (Occurs_In_N x (theta' a ms)).

Lemma OI_theta :
	((m:M)(oi_theta m))/\
	 ((ms:Ms)(oi_theta' ms)).

Lemma OI_Theta :
	(m:M)(x:V)
	 (Occurs_In_M x m)->
	  (Occurs_In_N x (theta m)).

Lemma OI_Theta' :
	(ms:Ms)(a:A)(x:V)
	 ((Occurs_In_Ms x ms)\/(Occurs_In_A x a))->
	  (Occurs_In_N x (theta' a ms)).

Definition oi_psi : N->Prop :=
	[n:N](x:V)
	 (Occurs_In_N x n)->
	  (Occurs_In_M x (psi n)).

Definition oi_psi' : A->Prop :=
	[a:A](ms:Ms)(x:V)
	 ((Occurs_In_A x a)\/(Occurs_In_Ms x ms))->
	  (Occurs_In_M x (psi' a ms)).

Lemma OI_psi :
	((n:N)(oi_psi n))/\
	 ((a:A)(oi_psi' a)).

Lemma OI_Psi :
	(n:N)(x:V)
	 (Occurs_In_N x n)->
	  (Occurs_In_M x (psi n)).

Lemma OI_Psi' :
	(a:A)(ms:Ms)(x:V)
	 ((Occurs_In_A x a)\/(Occurs_In_Ms x ms))->
	  (Occurs_In_M x (psi' a ms)).

Definition noi_theta : M->Prop :=
	[m:M](x:V)
	 ~(Occurs_In_M x m)->
	  ~(Occurs_In_N x (theta m)).

Definition noi_theta' : Ms->Prop :=
	[ms:Ms](x:V)(a:A)
	 ~(Occurs_In_Ms x ms)->
	  ~(Occurs_In_A x a)->
	   ~(Occurs_In_N x (theta' a ms)).

Lemma noi_Theta :
	((m:M)(noi_theta m))/\
	 ((ms:Ms)(noi_theta' ms)).

Lemma NOI_Theta :
	(x:V)(m:M)
	~(Occurs_In_M x m)->
	  ~(Occurs_In_N x (theta m)).

Lemma NOI_Theta' :
	(x:V)(a:A)(ms:Ms)
	 ~(Occurs_In_A x a)->
	  ~(Occurs_In_Ms x ms)->
	   ~(Occurs_In_N x (theta' a ms)).