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

(Intros n i j H; Cut (nat_compare2 j n); Auto; Unfold nat_compare2;
 Intros c; Case c;
 [ Clear  c; Intros c
 | Clear  c; Intros c; Case c;
   [ Clear  c; Intros c | Clear  c; Intros c ] ]).
(Unfold lift_V; Rewrite -> ltb_is_lt3).
(Unfold Setifb; Unfold Occurs_In_V1; Rewrite -> nateqb_is_eq3).
(Rewrite -> nateqb_is_eq3; Auto).
(Apply lt_not_eq1; Apply lt_trans with j:=j; Auto).

(Apply lt_not_eq1; Apply ltS; Apply lt_trans with j:=j; Auto).

(Apply ltnotlt; Auto).

(Unfold lift_V; Rewrite -> ltb_is_lt3).
(Unfold Setifb; Unfold Occurs_In_V1; Rewrite -> nateqb_is_eq3).
(Rewrite -> nateqb_is_eq3; Auto).
(Apply lt_not_eq1; Rewrite <- c; Auto).

(Rewrite <- c; Apply lt_not_eq1; Apply ltS; Auto).

(Apply notltii; Auto).

(Unfold lift_V; Rewrite -> ltb_is_lt1; Auto).
Save.

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

(Intros n i j H; Rewrite <- H; Clear  H).
(Unfold lift_V; Cut (nat_compare2 n i); Auto; Unfold nat_compare2;
 Auto;
 Intros d; Case d;
 [ Clear  d; Intros d
 | Clear  d; Intros d; Case d;
   [ Clear  d; Intros d | Clear  d; Intros d ] ]).
(Rewrite -> ltb_is_lt1; Auto; Simpl; Unfold Occurs_In_V1;
 Apply nateqb_is_eq3; Apply sym_not_equal).
(Apply lt_not_eq1; Auto).

Rewrite -> ltb_is_lt3.
(Simpl; Unfold Occurs_In_V1; Rewrite -> d; Apply nateqb_is_eq3; Auto).

(Apply notltii; Auto).

Rewrite -> ltb_is_lt3.
(Simpl; Unfold Occurs_In_V1; Apply nateqb_is_eq3;
 Apply lt_not_eq1; Apply ltS; Auto).

(Apply ltnotlt; Auto).
Save.

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

(Intros n i j H; Cut (nat_compare2 j n); Auto;
 Intros c; Case c;
 [ Clear  c; Intros c
 | Clear  c; Intros c; Case c;
   [ Clear  c; Intros c | Clear  c; Intros c ] ]).
(Unfold lift_V; Rewrite -> ltb_is_lt3).
(Unfold Setifb; Auto; Unfold Occurs_In_V1; Auto).

(Apply ltnotlt; Auto).

(Rewrite <- c; Clear  c n; Unfold lift_V; Rewrite -> ltb_is_lt3).
(Unfold Setifb; Auto).

(Apply notltii; Auto).

(Unfold lift_V; Rewrite -> ltb_is_lt1; Auto; Unfold Occurs_In_V1;
 Unfold Setifb; Rewrite -> nateqb_is_eq3).
(Rewrite -> nateqb_is_eq3; Auto).
(Apply sym_not_equal; Apply lt_not_eq1; Apply lt_trans with j:=j; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Apply ltS;
 Apply lt_trans with j:=j; Auto).
Save.

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

Intros.
Cut (or (eq ? (S j) i) (lt (S j) i)).
(Intros c; Case c; Clear  c; Intros).
(Generalize H; Clear  H; Rewrite <- H0; Clear  H0 i; Intros).
Clear  H.
Unfold pred.
(Cut (nat_compare2 j x); Auto; Unfold lift_V; Unfold nat_compare2;
 Intros c; Case c; Clear  c; Intros).
Rewrite -> ltb_is_lt3.
Unfold Setifb.
(Unfold Occurs_In_V1; Auto).

(Apply ltnotlt; Auto).

(Case H; Clear  H; Intros).
(Rewrite <- H; Clear  H x; Rewrite -> ltb_is_lt3).
Auto.

(Apply notltii; Auto).

(Rewrite -> ltb_is_lt1; Auto; Unfold Occurs_In_V1; Unfold Setifb ).
Rewrite -> nateqb_is_eq3.
(Rewrite -> nateqb_is_eq3; Auto).
(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Apply ltS; Auto).

(Clear  H; Inversion_clear H0).
(Unfold pred; Apply OI_Lift_V1_3; Auto).

(Apply lt_S_le; Auto).
Save.

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

(Apply M_Ms_ind; Unfold oi_lift_ms1_1; Unfold oi_lift_m1_1;
 Intros; Auto).
(Rewrite -> LIFTM1; Rewrite -> OIM1; Rewrite -> OIM1).
(Rewrite -> OI_Lift_V1_1; Auto; Rewrite -> H; Auto).

(Rewrite -> LIFTM2; Rewrite -> OIM2; Rewrite -> H; Auto).

(Rewrite -> LIFTM4; Rewrite -> OIM4; Rewrite -> H; Auto; Rewrite -> H0;
 Auto).
Save.

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

Cut ((m:M)(oi_lift_m1_1 m))/\
	 ((ms:Ms)(oi_lift_ms1_1 ms)).
Intros c; Case c; Auto.

Exact oi_lift_M1_1.
Save.

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

Cut ((m:M)(oi_lift_m1_1 m))/\
	 ((ms:Ms)(oi_lift_ms1_1 ms)).
Intros c; Case c; Auto.

Exact oi_lift_M1_1.
Save.

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

(Apply M_Ms_ind; Unfold oi_lift_ms1_2; Unfold oi_lift_m1_2;
 Intros; Auto).
(Rewrite -> LIFTM1; Rewrite -> OIM1; Rewrite -> H; Auto;
 Rewrite -> OI_Lift_V1_2; Auto).

(Rewrite -> LIFTM2; Rewrite -> OIM2; Rewrite -> H; Auto).

(Rewrite -> LIFTM4; Rewrite -> OIM4; Rewrite -> H; Auto; Rewrite -> H0;
 Auto).
Save.

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

Cut ((m:M)(oi_lift_m1_2 m))/\
	 ((ms:Ms)(oi_lift_ms1_2 ms)).
Intros c; Case c; Auto.

Exact oi_lift_M1_2.
Save.

Lemma OI_Lift_Ms1_2:
	(ms:Ms)(i,j:nat)
	 i=j->
	  (Occurs_In_Ms1 i (lift_Ms j ms))=false.
	
Cut ((m:M)(oi_lift_m1_2 m))/\
	 ((ms:Ms)(oi_lift_ms1_2 ms)).
Intros c; Case c; Auto.

Exact oi_lift_M1_2.
Save. 

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

(Apply M_Ms_ind; Unfold oi_lift_m1_3; Unfold oi_lift_ms1_3;
 Intros; Auto).
(Rewrite -> LIFTM1; Rewrite -> OIM1; Rewrite -> H; Auto;
 Rewrite -> OI_Lift_V1_3; Auto).

(Rewrite -> LIFTM2; Rewrite -> OIM2; Rewrite -> H; Auto).

(Rewrite -> LIFTM4; Rewrite -> OIM4; Rewrite -> H; Auto; Rewrite -> H0;
 Auto).
Save.

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

Cut ((m:M)(oi_lift_m1_3 m))/\
	 ((ms:Ms)(oi_lift_ms1_3 ms)).
Intros c; Case c; Auto.

Exact oi_lift_M1_3.
Save.

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

Cut ((m:M)(oi_lift_m1_3 m))/\
	 ((ms:Ms)(oi_lift_ms1_3 ms)).
Intros c; Case c; Auto.

Exact oi_lift_M1_3.
Save.

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

(Apply M_Ms_ind; Unfold oi_lift_ms1_4; Unfold oi_lift_m1_4;
 Intros; Auto).
(Rewrite -> LIFTM1; Rewrite -> OIM1; Rewrite -> H; Auto;
 Rewrite -> OI_Lift_V1_4; Auto).

(Rewrite -> LIFTM2; Rewrite -> OIM2; Rewrite -> H; Auto;
 Inversion_clear H0; Auto).

(Rewrite -> LIFTM4; Rewrite -> OIM4; Rewrite -> H; Auto; Rewrite -> H0;
 Auto).
Save.

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

Cut ((m:M)(oi_lift_m1_4 m))/\
	 ((ms:Ms)(oi_lift_ms1_4 ms)).
Intros c; Case c; Auto.

Exact oi_lift_M1_4.
Save.

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

Cut ((m:M)(oi_lift_m1_4 m))/\
	 ((ms:Ms)(oi_lift_ms1_4 ms)).
Intros c; Case c; Auto.

Exact oi_lift_M1_4.
Save.

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

(Apply N_A_ind; Unfold oi_lift_n1_1; Unfold oi_lift_a1_1; Intros).
(Rewrite -> LIFTN1; Rewrite -> OIN1; Rewrite -> H; Auto).

(Rewrite -> LIFTN2; Rewrite -> OIN2; Rewrite -> H; Auto).

(Rewrite -> LIFTN3; Rewrite -> OIN3; Rewrite -> H; Auto; Rewrite -> H0;
 Auto).

(Rewrite -> LIFTN4; Rewrite -> OIN4; Rewrite -> OI_Lift_V1_1; Auto).
Save.

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

Cut ((n:N)(oi_lift_n1_1 n))/\
	 ((a:A)(oi_lift_a1_1 a)).
Intros c; Case c; Auto.

Exact oi_lift_N1_1.
Save.

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

Cut ((n:N)(oi_lift_n1_1 n))/\
	 ((a:A)(oi_lift_a1_1 a)).
Intros c; Case c; Auto.

Exact oi_lift_N1_1.
Save.

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

(Apply N_A_ind; Unfold oi_lift_n1_2; Unfold oi_lift_a1_2; Intros).
(Rewrite -> LIFTN1; Rewrite -> OIN1; Rewrite -> H; Auto).

(Rewrite -> LIFTN2; Rewrite -> OIN2; Rewrite -> H; Auto).

(Rewrite -> LIFTN3; Rewrite -> OIN3; Rewrite -> H; Auto; Rewrite -> H0;
 Auto).

(Rewrite -> LIFTN4; Rewrite -> OIN4; Rewrite -> OI_Lift_V1_2; Auto).
Save.

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

Cut ((n:N)(oi_lift_n1_2 n))/\
	 ((a:A)(oi_lift_a1_2 a)).
Intros c; Case c; Auto.

Exact oi_lift_N1_2.
Save.

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

Cut ((n:N)(oi_lift_n1_2 n))/\
	 ((a:A)(oi_lift_a1_2 a)).
Intros c; Case c; Auto.

Exact oi_lift_N1_2.
Save.

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

(Apply N_A_ind; Unfold oi_lift_n1_3; Unfold oi_lift_a1_3; Intros).
(Rewrite -> LIFTN1; Rewrite -> OIN1; Rewrite -> H; Auto).

(Rewrite -> LIFTN2; Rewrite -> OIN2; Rewrite -> H; Auto).

(Rewrite -> LIFTN3; Rewrite -> OIN3; Rewrite -> H; Auto; Rewrite -> H0;
 Auto).

(Rewrite -> LIFTN4; Rewrite -> OIN4; Rewrite -> OI_Lift_V1_3; Auto).
Save.

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

Cut ((n:N)(oi_lift_n1_3 n))/\
	 ((a:A)(oi_lift_a1_3 a)).
Intros c; Case c; Auto.

Exact oi_lift_N1_3.
Save.

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

Cut ((n:N)(oi_lift_n1_3 n))/\
	 ((a:A)(oi_lift_a1_3 a)).
Intros c; Case c; Auto.

Exact oi_lift_N1_3.
Save.

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

(Apply N_A_ind; Unfold oi_lift_n1_4; Unfold oi_lift_a1_4; Intros).
(Rewrite -> LIFTN1; Rewrite -> OIN1; Rewrite -> H; Auto;
 Inversion_clear H0; Auto).

(Rewrite -> LIFTN2; Rewrite -> OIN2; Rewrite -> H; Auto).

(Rewrite -> LIFTN3; Rewrite -> OIN3; Rewrite -> H; Auto; Rewrite -> H0;
 Auto).

(Rewrite -> LIFTN4; Rewrite -> OIN4; Rewrite -> OI_Lift_V1_4; Auto).
Save.

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

Cut ((n:N)(oi_lift_n1_4 n))/\
	 ((a:A)(oi_lift_a1_4 a)).
Intros c; Case c; Auto.

Exact oi_lift_N1_4.
Save.

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

Cut ((n:N)(oi_lift_n1_4 n))/\
	 ((a:A)(oi_lift_a1_4 a)).
Intros c; Case c; Auto.

Exact oi_lift_N1_4.
Save.

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

(Induction l; Clear  l; Intros; Simpl).
(Rewrite -> OI_Lift_V1_4; Auto).

(Rewrite -> H; Auto; Rewrite -> H0; Auto).
(Rewrite -> OI_Lift_V1_4; Auto).
(Inversion_clear H1; Auto).

(Rewrite -> H; Inversion_clear H0; Auto).
Save.

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

(Apply M_Ms_ind; Unfold noi_msub_b_bridge; Unfold noi_mssub_b_bridge;
 Intros; Auto).
(Rewrite -> MSVMV1; Rewrite -> nateqb_is_eq3).
(Unfold Setifb; Rewrite -> H; Auto).

(Unfold not; Intros; Apply H0; Auto).

(Unfold not; Intros; Apply H0; Auto).

(Rewrite -> MSVMV2; Rewrite -> H; Auto).
(Unfold not; Intros; Apply H0; Auto).

(Rewrite -> MSVMV4; Rewrite -> H; Auto).
(Rewrite -> H0; Auto).
(Unfold not; Intros; Apply H1; Auto).

(Unfold not; Intros; Apply H1; Auto).
Save.

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

Cut ((m:M)(noi_msub_b_bridge m))/\
	 ((ms:Ms)(noi_mssub_b_bridge ms)).
Intros c; Case c; Auto.
Exact noi_msub_b_Bridge.
Save.

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

Cut ((m:M)(noi_msub_b_bridge m))/\
	 ((ms:Ms)(noi_mssub_b_bridge ms)).
Intros c; Case c; Auto.
Exact noi_msub_b_Bridge.
Save.

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

(Intros k i j H H0; Unfold 1 drop_V; Unfold 2 lift_V;
 Cut (nat_compare2 k (S i)); Auto; Unfold nat_compare2; Intros c;
 Case c; Clear  c; Intros).
(Cut (nat_compare2 k j); Auto; Unfold nat_compare2; Intros c; Case c;
 Clear  c; Intros).
(Rewrite -> ltb_is_lt1; Auto; Rewrite -> ltb_is_lt1; Auto).
(Unfold Setifb; Unfold lift_V; Unfold drop_V).
Cut (S k)=(S i)\/(lt (S k) (S i)).
(Intros c; Case c; Clear  c; Intros).
(Injection H3; Clear  H3; Intros).
Cut False.
Contradiction.

(Cut ~(lt k j); Intros).
(Apply H4; Auto).

(Rewrite -> H3; Apply ltnotlt; Auto).

(Inversion_clear H3; Rewrite -> ltb_is_lt1; Auto;
 Rewrite -> ltb_is_lt1; Auto).

(Apply lt_S_le; Auto).

(Case H2; Clear  H2; Intros).
Cut False.
Contradiction.

(Apply H0; Auto).

Rewrite -> ltb_is_lt3.
(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb; Unfold lift_V;
 Unfold drop_V).
Rewrite -> ltb_is_lt1.
Rewrite -> ltb_is_lt3.
Auto.

(Apply ltnotlt; Auto).

(Generalize H1 ; Clear  H1; Inversion_clear H2; Simpl; Intros).
(Inversion_clear H1; Auto).

(Inversion_clear H2; Auto).

(Apply ltnotlt; Auto).

(Case H1; Clear  H1; Intros).
Rewrite -> ltb_is_lt3.
Rewrite -> ltb_is_lt3.
(Rewrite -> H1; Unfold pred; Unfold Setifb; Unfold lift_V;
 Unfold drop_V).
Repeat (Rewrite -> ltb_is_lt3; Auto).

(Apply notltii; Auto).

(Rewrite -> H1; Apply ltnotlt; Auto).

Repeat (Rewrite -> ltb_is_lt3; Auto).
(Simpl; Unfold lift_V; Unfold drop_V).
Repeat (Rewrite -> ltb_is_lt3; Auto).
(Inversion_clear H1; Auto).

(Apply ltnotlt; Apply lt_trans with j:=i; Auto).
(Apply ltS; Apply Slt; Auto).

(Apply ltnotlt; Apply lt_trans with j:=(S i); Auto).
Save.

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

(Apply N_A_ind; Unfold lift_drop_n_bridge1;
 Unfold lift_drop_a_bridge1; Intros).
(Rewrite -> DROPN1; Rewrite -> LIFTN1; Rewrite -> LIFTN1;
 Rewrite -> DROPN1; Rewrite -> H; Auto; Unfold not  in H1; Unfold not;
 Intros; Apply H1; Auto).

(Rewrite -> DROPN2; Rewrite -> LIFTN2; Rewrite -> LIFTN2;
 Rewrite -> DROPN2; Rewrite -> H; Auto; Unfold not  in H1; Unfold not;
 Intros; Apply H1; Auto).

(Rewrite -> DROPN3; Rewrite -> LIFTN3; Rewrite -> LIFTN3;
 Rewrite -> DROPN3).
(Rewrite -> H; Auto).
(Rewrite -> H0; Auto; Unfold not  in H2; Unfold not; Intros; Apply H2;
 Auto).

(Unfold not  in H2; Unfold not; Intros; Apply H2; Auto).

(Rewrite -> DROPN4; Rewrite -> LIFTN4; Rewrite -> LIFTN4;
 Rewrite -> DROPN4; Rewrite -> Lift_Drop_V_Bridge1; Auto).
(Unfold not  in H0; Unfold not; Intros; Apply H0; Auto).
Save.

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

Cut ((n:N)(lift_drop_n_bridge1 n))/\((a:A)(lift_drop_a_bridge1 a)).
Unfold lift_drop_n_bridge1; Intros c; Case c; Intros; Auto.
Exact lift_drop_n_Bridge1.
Save.

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

Cut ((n:N)(lift_drop_n_bridge1 n))/\((a:A)(lift_drop_a_bridge1 a)).
Unfold lift_drop_a_bridge1; Intros c; Case c; Intros; Auto.
Exact lift_drop_n_Bridge1.
Save.

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

Intros.
Cut ~i=x.
(Clear  H; Intros).
Unfold 1 lift_V.
(Cut (nat_compare2 x j); Auto; Unfold nat_compare2; Intros c; Case c;
 Clear  c; Intros).
(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb; Unfold drop_V).
Repeat (Rewrite -> ltb_is_lt1; Auto).
(Simpl; Unfold lift_V; Rewrite -> ltb_is_lt1; Auto).

(Apply lt_trans3 with j:=j; Auto).

(Apply lt_trans2 with j:=j; Auto).

(Case H1; Clear  H1; Intros; Repeat (Rewrite -> ltb_is_lt3; Auto);
 Simpl; Unfold drop_V).
Repeat (Rewrite -> ltb_is_lt1; Auto).
(Simpl; Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).

(Rewrite -> H1; Apply ltS_neq_lt; Auto).
(Rewrite <- H1; Auto).

(Apply lt_S; Rewrite -> H1; Apply ltS_neq_lt; Auto).
(Rewrite <- H1; Auto).

(Cut (nat_compare2 x i); Auto; Unfold nat_compare2; Intros c; Case c;
 Clear  c; Intros).
(Rewrite -> ltb_is_lt1; Auto; Simpl; Unfold lift_V).
(Rewrite -> (ltb_is_lt1 x i H2); Simpl).
(Rewrite -> ltb_is_lt3; Auto).

(Case H2; Clear  H2; Intros; Repeat (Rewrite -> ltb_is_lt3; Auto);
 Simpl; Unfold lift_V).
Rewrite -> ltb_is_lt3.
(Inversion_clear H1; Auto).

(Apply lt_not_ltpred; Auto).

Rewrite -> ltb_is_lt3.
(Inversion_clear H1; Auto).

(Apply lt_not_ltpred; Auto).

(Unfold not; Intros; Auto_Contra H).
Save.

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

(Apply N_A_ind; Unfold drop_lift_n_bridge1; Unfold drop_lift_a_bridge1;
 Intros; Auto).
(Simpl; Rewrite -> H; Auto).
(Unfold not; Intros; Apply H0; Auto).

(Rewrite -> LIFTN2; Rewrite -> DROPN2; Rewrite -> H; Auto).
(Unfold not; Intros; Apply H0; Auto).

(Rewrite -> LIFTN3; Rewrite -> DROPN3; Rewrite -> H; Auto).
(Rewrite -> H0; Auto).
(Unfold not; Intros; Apply H1; Auto).

(Unfold not; Intros; Apply H1; Auto).

(Simpl; Rewrite -> Drop_Lift_V_Bridge1; Auto).
(Unfold not; Intros; Apply H; Auto).
Save.

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

Cut ((n:N)(drop_lift_n_bridge1 n))/\
	 ((a:A)(drop_lift_a_bridge1 a)).
Intros c; Case c; Auto.
Exact drop_lift_n_Bridge1.
Save.

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

Cut ((n:N)(drop_lift_n_bridge1 n))/\
	 ((a:A)(drop_lift_a_bridge1 a)).
Intros c; Case c; Auto.
Exact drop_lift_n_Bridge1.
Save.

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

(Intros n i j a H; Unfold 1 VsubstAV; Cut (nat_compare2 i n); Auto;
 Unfold nat_compare2; Intros c; Case c; Clear  c; Intros).
(Rewrite -> nateqb_is_eq3; Auto).
(Unfold Setifb; Unfold drop_V; Rewrite -> ltb_is_lt3; Auto).
(Simpl; Unfold lift_V).
(Cut (nat_compare2 n (S j)); Auto; Unfold nat_compare2; Intros c;
 Case c; Clear  c; Intros).
(Rewrite -> ltb_is_lt1; Auto).
(Rewrite -> ltb_is_lt1; Auto).
(Simpl; Unfold VsubstAV; Rewrite -> nateqb_is_eq3; Auto).
(Simpl; Unfold drop_V; Rewrite -> ltb_is_lt3; Auto).

(Apply lt_not_eq1; Auto).

(Generalize H1 ; Clear  H1; Inversion_clear H0; Intros).
(Inversion_clear H1; Auto).

(Inversion_clear H0; Auto).

(Case H1; Clear  H1; Intros; Repeat (Rewrite -> ltb_is_lt3; Auto)).
(Simpl; Unfold VsubstAV).
(Rewrite -> nateqb_is_eq3; Auto).
Unfold drop_V.
(Rewrite -> ltb_is_lt3; Auto).
Simpl.
(Inversion_clear H0; Auto).

(Apply lt_not_eq1; Auto).

(Rewrite -> H1; Auto).

(Simpl; Unfold VsubstAV).
(Rewrite -> nateqb_is_eq3; Auto).
(Simpl; Unfold drop_V).
(Rewrite -> ltb_is_lt3; Auto).
(Inversion_clear H0; Auto).

(Apply lt_not_eq1; Auto).

(Apply lt_not_eq1; Auto).

(Case H0; Clear  H0; Intros).
(Rewrite -> nateqb_is_eq1; Auto; Simpl; Unfold lift_V).
(Rewrite -> ltb_is_lt1; Auto).
(Simpl; Unfold VsubstAV).
(Rewrite -> nateqb_is_eq1; Auto).

(Rewrite <- H0; Auto).

(Rewrite -> nateqb_is_eq3; Auto).
(Unfold Setifb; Unfold drop_V; Unfold lift_V).
Repeat (Rewrite -> ltb_is_lt1; Auto).
(Simpl; Unfold VsubstAV).
Rewrite -> nateqb_is_eq3.
(Simpl; Unfold lift_V; Unfold drop_V).
Repeat (Rewrite -> ltb_is_lt1; Auto).
(Apply lt_trans with j:=i; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Apply lt_trans with j:=i; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).
Save.

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

(Apply N_A_ind; Unfold lift_nsub_b_bridge0;
 Unfold lift_asub_b_bridge0; Intros).
(Rewrite -> NSAV1; Rewrite -> LIFTN1; Rewrite -> H; Auto;
 Rewrite <- Lift_Lift_A_Bridge; Auto; Inversion_clear H0; Auto).

(Rewrite -> NSAV2; Rewrite -> LIFTN2; Rewrite -> H; Auto).

(Rewrite -> NSAV3; Rewrite -> LIFTN3; Rewrite -> H; Auto;
 Rewrite -> H0; Auto).

(Rewrite -> NSAV4; Rewrite -> LIFTN4;
 Rewrite -> Lift_Vsub_Bridge0; Auto).
Save.

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

Cut ((n:N)(lift_nsub_b_bridge0 n))/\ ((a:A)(lift_asub_b_bridge0 a)).
Unfold lift_nsub_b_bridge0.
Intros c; Case c; Intros; Auto.
Exact lift_nsub_b_Bridge0.
Save.

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

Cut ((n:N)(lift_nsub_b_bridge0 n))/\ ((a:A)(lift_asub_b_bridge0 a)).
Unfold lift_asub_b_bridge0.
Intros c; Case c; Intros; Auto.
Exact lift_nsub_b_Bridge0.
Save.

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

(Intros; Rewrite <- (psitheta m0); Rewrite <- (psitheta m);
 Rewrite -> Msub_Psi_Bridge; Rewrite -> Lift_Psi_Bridge;
 Rewrite -> Lift_Nsub_Bridge0; Auto; Rewrite -> LIFTN3;
 Rewrite -> (Lift_Theta_Bridge m0); Rewrite -> Lift_Theta_Bridge;
 Rewrite -> LIFTN4; Rewrite <- Msub_Psi_Bridge; Rewrite -> psitheta;
 Rewrite -> psitheta; Rewrite -> psitheta; Rewrite -> psitheta; Auto).
Save.

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

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

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

(Apply M_Ms_ind; Unfold lift_msub_bridge2; Unfold lift_mssub_bridge2;
 Auto; Intros).
(Repeat Rewrite -> LIFTM1; Unfold 2 4 lift_V;
 Cut (nat_compare2 (S y) v);
 [ Destruct 1; [ Intro | Destruct 1; Intro ] | Auto ]).
(Rewrite -> ltb_is_lt3; Unfold Setifb; Unfold lift_V).
(Repeat Rewrite -> ltb_is_lt3; Unfold Setifb).
Repeat Rewrite -> MSVMV1.
(Repeat Rewrite -> nateqb_is_eq3; Unfold Setifb; Unfold drop_V).
(Repeat Rewrite -> ltb_is_lt3; Unfold Setifb; Unfold pred).
(Rewrite -> H; Auto).

(Apply ltnotlt; Apply ltS; Apply ltS; Apply Slt; Auto).

(Apply ltnotlt; Apply ltS; Apply ltS; Auto).

(Apply lt_not_eq1; Apply ltS; Apply ltS; Apply Slt; Auto).

(Apply lt_not_eq1; Apply ltS; Apply ltS; Auto).

(Apply ltnotlt; Auto).

(Apply ltnotlt; Apply ltS; Apply Slt; Auto).

(Apply ltnotlt; Auto).

(Rewrite <- H2; Clear  H0 H1 H2 v).
(Rewrite -> ltb_is_lt3; Unfold Setifb; Unfold lift_V).
(Repeat Rewrite -> ltb_is_lt3; Unfold Setifb).
(Repeat Rewrite -> MSVMV1; Repeat Rewrite -> nateqb_is_eq3;
 Unfold Setifb).
Unfold drop_V.
(Repeat Rewrite -> ltb_is_lt3; Unfold Setifb).
(Rewrite -> H; Auto).

(Apply ltnotlt; Apply ltS; Apply ltS; Apply ltiSi; Auto).

(Apply ltnotlt; Apply ltS; Apply ltiSi; Auto).

(Apply lt_not_eq1; Apply ltS; Apply ltS; Apply ltiSi; Auto).

(Apply lt_not_eq1; Apply ltS; Apply ltiSi; Auto).

(Apply notltii; Auto).

(Apply ltnotlt; Apply ltS; Apply ltiSi; Auto).

(Apply notltii; Auto).

Clear  H0 H1.
(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb; Unfold lift_V).
(Cut (nat_compare v y); [ Destruct 1; Intro | Auto ]).
Rewrite -> ltb_is_lt3.
(Rewrite -> ltb_is_lt1; Unfold Setifb).
Repeat Rewrite -> MSVMV1.
(Repeat Rewrite -> nateqb_is_eq1; Auto).
Unfold Setifb.
(Rewrite -> H1; Rewrite -> H; Auto).

(Rewrite -> H1; Apply ltS; Auto).

(Apply notltii; Auto).

(Repeat Rewrite -> ltb_is_lt1; Unfold Setifb).
Repeat Rewrite -> MSVMV1.
(Repeat Rewrite -> nateqb_is_eq3; Auto; Unfold Setifb; Unfold drop_V).
(Repeat Rewrite -> ltb_is_lt1; Auto; Unfold Setifb).
(Rewrite -> H; Auto).

(Apply ltS_neq_lt; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Apply ltS; Auto).

(Apply ltS_neq_lt; Auto).

(Repeat Rewrite -> LIFTM2; Repeat Rewrite -> MSVMV2; Rewrite -> H; Auto).

(Repeat Rewrite -> LIFTM4; Repeat Rewrite -> MSVMV4; Rewrite -> H;
 Rewrite -> H0; Auto).
Save.

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

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

Intros c; Case c; Unfold lift_msub_bridge2; Auto.
Exact Lift_msub_bridge2.
Save.

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

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

Intros c; Case c; Unfold lift_mssub_bridge2; Auto.
Exact Lift_msub_bridge2.
Save.

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

(Intros n i j a H; Rewrite -> H; Clear  H i).
(Unfold lift_V; Unfold 1 VsubstAV; Unfold drop_V;
 Cut (nat_compare2 n j); Auto; Unfold nat_compare2; Intros c; Case c;
 Clear  c; Intros).
(Rewrite -> ltb_is_lt1; Auto; Rewrite -> nateqb_is_eq3).
(Rewrite -> ltb_is_lt1; Auto).
(Simpl; Unfold VsubstAV).
Rewrite -> nateqb_is_eq3.
(Simpl; Unfold lift_V; Unfold drop_V).
(Rewrite -> ltb_is_lt1; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Case H; Clear  H; Intros).
(Rewrite -> ltb_is_lt3; Auto; Rewrite -> ltb_is_lt1; Auto; Simpl).
Unfold VsubstAV.
(Rewrite -> nateqb_is_eq1; Auto).

Repeat (Rewrite -> ltb_is_lt3; Auto).
(Simpl; Unfold VsubstAV).
Repeat (Rewrite -> nateqb_is_eq3; Auto).
(Simpl; Unfold lift_V; Unfold drop_V).
Repeat (Rewrite -> ltb_is_lt3; Auto).
(Simpl; Inversion_clear H; Auto).

(Apply lt_not_ltpred; Auto).

(Apply lt_not_eq1; Auto).

(Apply lt_not_eq1; Auto).

(Apply lt_not_ltS; Auto).
Save.

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

(Intros n i j a H; Unfold lift_V; Cut (nat_compare2 n j); Auto;
 Unfold nat_compare2; Intros c; Case c; Clear  c; Intros).
(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb; Unfold VsubstAV).
Rewrite -> nateqb_is_eq3.
Rewrite -> nateqb_is_eq3.
(Unfold Setifb; Unfold drop_V).
Rewrite -> ltb_is_lt1.
Rewrite -> ltb_is_lt1.
Unfold Setifb.
(Rewrite -> LIFTN4; Unfold lift_V).
(Rewrite -> ltb_is_lt1; Auto).

(Apply lt_trans with j:=j; Auto; Apply ltS; Auto).

(Apply lt_trans with j:=j; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Apply lt_trans with j:=j; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Apply lt_trans with j:=j; Auto).

(Case H0; Clear  H0; Intros).
(Rewrite -> H0; Clear  H0 n).
(Rewrite -> ltb_is_lt3; Auto; Simpl; Unfold VsubstAV).
Repeat (Rewrite -> nateqb_is_eq3; Auto).
(Simpl; Unfold drop_V).
(Repeat (Rewrite -> ltb_is_lt1; Auto); Simpl; Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Rewrite -> ltb_is_lt3; Auto; Simpl; Unfold VsubstAV).
(Cut (nat_compare2 i n); Auto; Unfold nat_compare2; Intros c; Case c;
 Clear  c; Intros).
Repeat (Rewrite -> nateqb_is_eq3; Auto).
(Simpl; Unfold drop_V).
Repeat (Rewrite -> ltb_is_lt3; Auto).
(Simpl; Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).
(Inversion_clear H0; Auto).

(Apply lt_not_ltpred; Auto).

(Apply lt_not_eq1; Auto).

(Apply lt_not_eq1; Auto).

(Case H1; Clear  H1; Intros).
(Rewrite -> nateqb_is_eq1; Auto; Simpl).
(Rewrite -> nateqb_is_eq1; Auto).

Repeat (Rewrite -> nateqb_is_eq3; Auto).
(Simpl; Unfold drop_V).
(Repeat (Rewrite -> ltb_is_lt1; Auto); Simpl; Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).
Save.

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

(Apply N_A_ind; Unfold lift_nsub_b_bridge1;
 Unfold lift_asub_b_bridge1; Intros).
(Rewrite -> H0; Clear  H0 i; Rewrite -> NSAV1; 
 Rewrite -> LIFTN1; Rewrite -> H; Auto; Elim j).
(Rewrite <- Lift_Lift_A_Bridge1; Auto).

(Intros; Rewrite <- Lift_Lift_A_Bridge; Auto).

(Rewrite -> NSAV2; Rewrite -> LIFTN2; Rewrite -> H; Auto).

(Rewrite -> NSAV3; Rewrite -> LIFTN3; Rewrite -> H; Auto;
 Rewrite -> H0; Auto).

(Rewrite -> NSAV4; Rewrite -> LIFTN4; Rewrite -> Lift_Vsub_Bridge1;
 Auto).
Save.

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

Cut ((n:N)(lift_nsub_b_bridge1 n))/\ ((a:A)(lift_asub_b_bridge1 a)).
Unfold lift_nsub_b_bridge1.
Intros c; Case c; Intros; Auto.
Exact lift_nsub_b_Bridge1.
Save.

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

Cut ((n:N)(lift_nsub_b_bridge1 n))/\ ((a:A)(lift_asub_b_bridge1 a)).
Unfold lift_asub_b_bridge1.
Intros c; Case c; Intros; Auto.
Exact lift_nsub_b_Bridge1.
Save.

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

(Apply N_A_ind; Unfold lift_nsub_b_bridge2;
 Unfold lift_asub_b_bridge2; Intros; Auto).
(Rewrite -> NSAV1; Rewrite -> LIFTN1; Rewrite -> H; Auto;
 Rewrite -> LIFTN1; Rewrite -> NSAV1).
Elim j.
(Rewrite <- Lift_Lift_A_Bridge1; Auto).

(Intros; Rewrite <- Lift_Lift_A_Bridge; Auto).

(Rewrite -> NSAV2; Rewrite -> LIFTN2; Rewrite -> H; Auto).

(Rewrite -> NSAV3; Rewrite -> LIFTN3; Rewrite -> H; Auto;
 Rewrite -> H0; Auto).

(Rewrite -> NSAV4; Rewrite -> LIFTN4; Rewrite -> Lift_Vsub_Bridge2;
 Auto).
Save.

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

Cut ((n:N)(lift_nsub_b_bridge2 n))/\ ((a:A)(lift_asub_b_bridge2 a)).
Intros c; Case c; Auto.
Exact lift_nsub_b_Bridge2.
Save.

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

Cut ((n:N)(lift_nsub_b_bridge2 n))/\ ((a:A)(lift_asub_b_bridge2 a)).
Intros c; Case c; Auto.
Exact lift_nsub_b_Bridge2.
Save.

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

(Intros n i j a H; Rewrite -> H; Clear  H i; Cut (nat_compare2 n j);
 Auto; Unfold nat_compare2; Intros c; Case c; Clear  c; Intros).
(Unfold lift_V; Rewrite -> ltb_is_lt1; Auto; Unfold Setifb;
 Unfold VsubstAV).
Repeat (Rewrite -> nateqb_is_eq3; Auto).
(Simpl; Unfold drop_V).
(Repeat (Rewrite -> ltb_is_lt1; Auto); Simpl; Unfold lift_V).
(Rewrite -> ltb_is_lt1; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Unfold lift_V; Case H; Clear  H; Intros;
 Repeat (Rewrite -> ltb_is_lt3; Auto); Simpl; Unfold VsubstAV).
Repeat (Rewrite -> nateqb_is_eq1; Auto).

Repeat (Rewrite -> nateqb_is_eq3; Auto).
(Simpl; Unfold drop_V).
(Repeat (Rewrite -> ltb_is_lt3; Auto); Simpl; Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).
(Inversion_clear H; Auto).

(Apply lt_not_ltpred; Auto).

(Apply lt_not_eq1; Auto).

(Apply lt_not_eq1; Auto).
Save.

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

(Apply N_A_ind; Unfold lift_nsub_b_bridge3;
 Unfold lift_asub_b_bridge3; Intros).
(Rewrite -> H0; Clear  H0 i; Rewrite -> NSAV1; 
 Rewrite -> LIFTN1; Rewrite -> H; Auto; Elim j).
(Rewrite <- Lift_Lift_A_Bridge1; Auto).

(Intros; Rewrite <- Lift_Lift_A_Bridge; Auto).

(Rewrite -> NSAV2; Rewrite -> LIFTN2; Rewrite -> H; Auto).

(Rewrite -> NSAV3; Rewrite -> LIFTN3; Rewrite -> H; Auto;
 Rewrite -> H0; Auto).

(Rewrite -> NSAV4; Rewrite -> LIFTN4; Rewrite -> Lift_Vsub_Bridge3;
 Auto).
Save.

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

Cut ((n:N)(lift_nsub_b_bridge3 n))/\ ((a:A)(lift_asub_b_bridge3 a)).
Unfold lift_nsub_b_bridge3.
Intros c; Case c; Intros; Auto.
Exact lift_nsub_b_Bridge3.
Save.

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

Cut ((n:N)(lift_nsub_b_bridge3 n))/\ ((a:A)(lift_asub_b_bridge3 a)).
Unfold lift_asub_b_bridge3.
Intros c; Case c; Intros; Auto.
Exact lift_nsub_b_Bridge3.
Save.

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

(Intros; Rewrite <- (psitheta m0); Rewrite <- (psitheta m);
 Rewrite -> Msub_Psi_Bridge; Rewrite -> Lift_Psi_Bridge;
 Rewrite -> Lift_Nsub_Bridge1; Auto; Rewrite -> LIFTN3;
 Rewrite -> (Lift_Theta_Bridge m0); Rewrite -> Lift_Theta_Bridge;
 Rewrite -> LIFTN4; Rewrite <- Msub_Psi_Bridge; Rewrite -> psitheta;
 Rewrite -> psitheta; Rewrite -> psitheta; Rewrite -> psitheta; Auto).
Save.

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

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

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

(Induction l; Clear  l; Auto; Intros).
(Rewrite -> lift_L_eq2; Rewrite -> phi_eq2; Rewrite -> phi_eq2).
(Elim i; Intros).
(Rewrite <- H; Rewrite <- H0).
(Rewrite <- LIFTN4; Rewrite <- LIFTN3).
(Rewrite -> Lift_Nsub_Bridge1; Auto).

(Rewrite -> Lift_Nsub_Bridge0; Auto; Rewrite -> LIFTN3; 
 Rewrite -> LIFTN4; Rewrite -> H0; Rewrite -> H; Auto).

(Simpl; Rewrite -> H; Auto).
Save.

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

(Intros; Rewrite <- psiphiphibar; Rewrite -> Lift_Psi_Bridge;
 Rewrite -> Lift_Phi_Bridge; Rewrite -> psiphiphibar; Auto).
Save.

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

(Induction l; Clear  l; Intros; Simpl).
(Rewrite -> Drop_Lift_V; Auto).

(Rewrite -> H; Rewrite -> H0; Rewrite -> Drop_Lift_V; Auto).

(Rewrite -> H; Auto).
Save.

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

(Apply M_Ms_ind; Unfold oi_theta; Unfold oi_theta'; Intros).
(Rewrite -> th1; Apply H; Inversion_clear H0; Auto).

(Rewrite -> th2; Apply Occurs_in_lam; Apply H; Inversion_clear H0; Auto).

(Simpl; Inversion_clear H; Auto; Inversion H0).

(Rewrite -> th4; Inversion_clear H1).
(Inversion_clear H2; Apply H0; Auto).

(Apply H0; Auto).
Save.

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

Cut ((m:M)(oi_theta m))/\
	 ((ms:Ms)(oi_theta' ms)).
Intros c; Case c; Clear c; Auto.

Exact OI_theta.
Save.

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

Cut ((m:M)(oi_theta m))/\
	 ((ms:Ms)(oi_theta' ms)).
Intros c; Case c; Clear c; Auto.
Exact OI_theta.
Save.

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

(Apply N_A_ind; Unfold oi_psi; Unfold oi_psi'; Intros).
(Simpl; Inversion_clear H0; Apply Occurs_in_lambda; Apply H; Auto).

(Rewrite -> ps2; Inversion_clear H0; Apply H; Auto).

(Rewrite -> ps3; Inversion_clear H1; Auto).
(Apply H; Auto).
(Inversion_clear H2; Auto).

(Inversion_clear H; Simpl; Auto).
(Inversion_clear H0; Auto).
Save.

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

Cut ((n:N)(oi_psi n))/\((a:A)(oi_psi' a)).
(Intros c; Case c; Auto).

Exact OI_psi.
Save.

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

Cut ((n:N)(oi_psi n))/\((a:A)(oi_psi' a)).
(Intros c; Case c; Auto).

Exact OI_psi.
Save.

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

(Apply M_Ms_ind; Unfold noi_theta; Unfold noi_theta'; Intros; Auto).
Rewrite -> th1.
(Apply H; Unfold not; Intros; Apply H0; Auto).
(Inversion_clear H1; Auto).

(Rewrite -> th2; Apply OIN1_is_OIN4; Rewrite -> OIN1;
 Apply OIN1_is_OIN3; Apply H; Unfold not; Intros; Apply H0; Auto).

(Rewrite -> th3; Unfold not; Intros; Apply H0; Inversion_clear H1; Auto).

(Rewrite -> th4; Apply H0; Auto).
(Unfold not; Intros; Apply H1; Auto).

(Apply OIA1_is_OIA4; Rewrite -> OIN3; Apply ororb1; Split).
(Apply OIA1_is_OIA3; Auto).

(Apply OIN1_is_OIN3; Apply H; Auto).
(Unfold not; Intros; Apply H1; Auto).
Save.

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

Cut ((m:M)(noi_theta m))/\
	 ((ms:Ms)(noi_theta' ms)).
Intros c; Case c; Unfold noi_theta; Auto.
Exact noi_Theta.
Save.

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

Cut ((m:M)(noi_theta m))/\
	 ((ms:Ms)(noi_theta' ms)).
Intros c; Case c; Unfold noi_theta'; Auto.
Exact noi_Theta.
Save.