Require MinMJ_Lift.
Require MinMJ_Drop.

Inductive
    Occurs_In_V : nat->V->Prop :=
	Occurs_in_v : (i,j:nat)i=j->
		       (Occurs_In_V i j).

Inductive
    Occurs_In_L : nat->L->Prop :=
	Occurs_in_vr :
		(i:nat)(x:V)
		 (Occurs_In_V i x)->
		  (Occurs_In_L i (vr x)) |
	Occurs_in_app1 :
		(i:nat)(x:V)(l1,l2:L)
		 (Occurs_In_V i x)->
		  (Occurs_In_L i (app x l1 l2)) |
	Occurs_in_app2 :
		(i:nat)(x:V)(l1,l2:L)
		 (Occurs_In_L i l1)->
		  (Occurs_In_L i (app x l1 l2)) |
	Occurs_in_app3 :
		(i:nat)(x:V)(l1,l2:L)
		 (Occurs_In_L (S i) l2)->
		  (Occurs_In_L i (app x l1 l2)) |
	Occurs_in_lm :
		(i:nat)(l:L)
		 (Occurs_In_L (S i) l)->
		  (Occurs_In_L i (lm l)).

Mutual Inductive
    Occurs_In_M : nat->M->Prop :=
	Occurs_in_sc1 :
		(i:nat)(x:V)(ms:Ms)
		 (Occurs_In_V i x)->
		  (Occurs_In_M i (sc x ms)) |
	Occurs_in_sc2 :
		(i:nat)(x:V)(ms:Ms)
		 (Occurs_In_Ms i ms)->
		  (Occurs_In_M i (sc x ms)) |
	Occurs_in_lambda :
		(i:nat)(m:M)
		 (Occurs_In_M (S i) m)->
		  (Occurs_In_M i (lambda m))
with
    Occurs_In_Ms : nat->Ms->Prop :=
	Occurs_in_mcons1 :
		(i:nat)(m:M)(ms:Ms)
		 (Occurs_In_M i m)->
		  (Occurs_In_Ms i (mcons m ms)) |
	Occurs_in_mcons2 :
		(i:nat)(m:M)(ms:Ms)
		 (Occurs_In_Ms i ms)->
		  (Occurs_In_Ms i (mcons m ms)).

Mutual Inductive
    Occurs_In_N : nat->N->Prop :=
	Occurs_in_lam :
		(i:nat)(n:N)
		 (Occurs_In_N (S i) n)->
		  (Occurs_In_N i (lam n)) |
	Occurs_in_an :
		(i:nat)(a:A)
		 (Occurs_In_A i a)->
		  (Occurs_In_N i (an a))
with
    Occurs_In_A : nat->A->Prop :=
	Occurs_in_ap1 :
		(i:nat)(a:A)(n:N)
		 (Occurs_In_A i a)->
		  (Occurs_In_A i (ap a n)) |
	Occurs_in_ap2 :
		(i:nat)(a:A)(n:N)
		 (Occurs_In_N i n)->
		  (Occurs_In_A i (ap a n)) |
	Occurs_in_var :
		(i:nat)(x:V)
		 (Occurs_In_V i x)->
		  (Occurs_In_A i (var x)).

Hint Occurs_in_v.
Hint Occurs_in_var.
Hint Occurs_in_vr.
Hint Occurs_in_sc1.
Hint Occurs_in_sc2.
Hint Occurs_in_lam.
Hint Occurs_in_lambda.
Hint Occurs_in_lm.
Hint Occurs_in_app1.
Hint Occurs_in_app2.
Hint Occurs_in_app3.
Hint Occurs_in_mcons1.
Hint Occurs_in_mcons2.
Hint Occurs_in_ap1.
Hint Occurs_in_ap2.
Hint Occurs_in_an.

Recursive Definition Occurs_In_V1 : V->V->bool :=
i j => (nateqb i j).

Lemma OIV1_is_OIV1 : (i,x:V)
		(Occurs_In_V i x)->
		 (Occurs_In_V1 i x)=true.

(Intros; Inversion_clear H; Exact (nateqb_is_eq1 i x H0)).
Save.

Lemma OIV1_is_OIV2 : (i:V)(x:V)
		(Occurs_In_V1 i x)=true->
		 (Occurs_In_V i x).

(Unfold Occurs_In_V1 ; Intros; Apply Occurs_in_v;
 Exact (nateqb_is_eq2 i x H)).
Save.

Lemma OIV1_is_OIV3 : (i:V)(x:V)
		~(Occurs_In_V i x)->
		 (Occurs_In_V1 i x)=false.
Unfold not.
Intros.
Apply bool_dec5.
(Unfold not ;Intros;Apply H).
Exact (OIV1_is_OIV2 i x H0).
Save.

Lemma OIV1_is_OIV4 : (i:V)(x:V)
		(Occurs_In_V1 i x)=false->
		 ~(Occurs_In_V i x).
Intros.
Cut (not (eq ? (Occurs_In_V1 i x) true)).
(Unfold not ;Intros;Apply H0).
Apply OIV1_is_OIV1.
Auto.

Apply bool_dec6.
Auto.
Save.

Definition OIV_compare : V->V->Prop :=
[i:V][x:V](Occurs_In_V i x)\/~(Occurs_In_V i x).

Lemma OIV_dec :
	(i:V)(x:V)
	 (OIV_compare i x).

Unfold OIV_compare.
Intros.
(Cut (nat_compare i x); Auto; Intros c; Case c; Clear  c; Intros; Auto).
(Right; Unfold not ; Intros; Apply H; Inversion_clear H0; Auto).
Save.

Recursive Definition
    Occurs_In_L1 : V->L->bool :=
	i (vr x) => (Occurs_In_V1 i x) |
	i (app  x l1 l2) =>
		(orb (Occurs_In_V1 i x)
		     (orb (Occurs_In_L1 i l1)
			  (Occurs_In_L1 (S i) l2))) |
	i (lm l) => (Occurs_In_L1 (S i) l).

Lemma OIL1_is_OIL1 :
	(l:L)(i:V)
	 (Occurs_In_L i l)->
	  (Occurs_In_L1 i l)=true.

(Induction l; Intros).
Inversion_clear H.
Exact (OIV1_is_OIV1 i v H0).

(Generalize H H0 ; Clear  H H0).
Inversion_clear H1.
Simpl.
Intros.
Rewrite -> (OIV1_is_OIV1 i v H).
Auto.

(Intros; Auto).
Simpl.
(Rewrite -> H0; Auto).
Simpl.
(Case (Occurs_In_V1 i v); Auto).

(Simpl; Intros).
(Rewrite -> H1; Auto).
(Case (Occurs_In_L1 i l0); Case (Occurs_In_V1 i v); Auto).

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

Lemma OIL1_is_OIL2 : (l:L)(i:V)
		(Occurs_In_L1 i l)=true->
		 (Occurs_In_L i l).

(Induction l; Simpl; Intros).
(Apply Occurs_in_vr; Apply OIV1_is_OIV2; Auto).

Cut (or (eq ? (Occurs_In_V1 i v) true)
      (or (eq ? (Occurs_In_L1 i l0) true)
        (eq ? (Occurs_In_L1 (S i) l1) true))).
(Intros c; Case c; Clear  c; Intros).
(Apply Occurs_in_app1; Apply OIV1_is_OIV2; Auto).

(Case H2; Clear  H2; Intros).
(Apply Occurs_in_app2; Apply H; Auto).

(Apply Occurs_in_app3; Apply H0; Auto).

(Generalize H1 ; Clear  H1; Case (Occurs_In_V1 i v); Auto).
(Case (Occurs_In_L1 i l0); Auto).

(Apply Occurs_in_lm; Apply H; Auto).
Save.

Lemma OIL1_is_OIL3 :
	(l:L)(i:V)
	 ~(Occurs_In_L i l)->
	  (Occurs_In_L1 i l)=false.
Unfold not.
Intros.
Apply bool_dec5.
Unfold not ;Intros;Apply H.
Exact (OIL1_is_OIL2 l i H0).
Save.

Lemma OIL1_is_OIL4 :
	(l:L)(i:V)
	 (Occurs_In_L1 i l)=false->
	  ~(Occurs_In_L i l).
Intros.
Cut (not (eq ? (Occurs_In_L1 i l) true)).
Unfold not ;Intros;Apply H0.
Apply OIL1_is_OIL1.
Auto.

Apply bool_dec6.
Auto.
Save.

Definition OIL_compare : V->L->Prop :=
[i:V][l:L](Occurs_In_L i l)\/~(Occurs_In_L i l).

Lemma OIL_dec :
	(l:L)(i:V)
	 (OIL_compare i l).

Unfold OIL_compare .
Intros.
Cut (or (eq ? (Occurs_In_L1 i l) true) (eq ? (Occurs_In_L1 i l) false)).
(Intros c; Case c; Clear  c; Intros).
(Left; Apply OIL1_is_OIL2; Auto).

(Right; Apply OIL1_is_OIL4; Auto).

(Case (Occurs_In_L1 i l); Auto).
Save.

Fixpoint
    Occurs_In_M2 [m:M] : V->bool :=
	[i:V]<bool>Case m of
	    (* x;ms *)[x:V][ms:Ms]
		(orb (Occurs_In_V1 i x) (Occurs_In_Ms2 ms i))
	    (* lambda m *)[m':M]
		(Occurs_In_M2 m' (S i))
end with
    Occurs_In_Ms2 [ms:Ms] : V->bool :=
	[i:V]<bool>Case ms of
	    (* mnil *)
		false
	    (* m::ms *)[m:M][ms':Ms]
		(orb (Occurs_In_M2 m i) (Occurs_In_Ms2 ms' i))
end.

Recursive Definition
    Occurs_In_M1 : V->M->bool :=
	x m => (Occurs_In_M2 m x).

Recursive Definition
    Occurs_In_Ms1 : V->Ms->bool :=
	x ms => (Occurs_In_Ms2 ms x).

Lemma OIM1 : (i,x:V)(ms:Ms)
	(Occurs_In_M1 i (sc x ms))
	=(orb (Occurs_In_V1 i x)
	      (Occurs_In_Ms1 i ms)).
Auto.
Save.

Lemma OIM2 : (i:V)(m:M)
	(Occurs_In_M1 i (lambda m))=
	 (Occurs_In_M1 (S i) m).
Auto.
Save.

Lemma OIM3 : (i:V)
	(Occurs_In_Ms1 i mnil)=false.
Auto.
Save.

Lemma OIM4 : (i:V)(m:M)(ms:Ms)
	(Occurs_In_Ms1 i (mcons m ms))=
	 (orb (Occurs_In_M1 i m)
		(Occurs_In_Ms1 i ms)).
Auto.
Save.

Definition oim1_is_oim1 : M->Prop :=
[m:M](i:V)(Occurs_In_M i m)->
	      (Occurs_In_M1 i m)=true.

Definition oims1_is_oims1 : Ms->Prop :=
[ms:Ms](i:V)(Occurs_In_Ms i ms)->
		(Occurs_In_Ms1 i ms)=true.

Lemma oiM1_is_oiM1 :
	((m:M)(oim1_is_oim1 m))/\
	 ((ms:Ms)(oims1_is_oims1 ms)).

(Apply M_Ms_ind; Unfold oims1_is_oims1 ; Unfold oim1_is_oim1 ; Intros).
Rewrite -> OIM1.
Inversion_clear H0.
Rewrite -> (OIV1_is_OIV1 i v H1).
Auto.

Rewrite -> (H i H1).
(Case (Occurs_In_V1 i v); Auto).

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

Inversion H.

(Rewrite -> OIM4; Apply ororb; Inversion_clear H1).
(Left; Apply H; Auto).

(Right; Apply H0; Auto).
Save.

Lemma OIM1_is_OIM1 : (i:V)(m:M)
(Occurs_In_M i m)->
	      (Occurs_In_M1 i m)=true.

Cut ((m:M)(oim1_is_oim1 m))/\
	 ((ms:Ms)(oims1_is_oims1 ms)).
Unfold oim1_is_oim1; Intros H; Case H; Auto.
Exact oiM1_is_oiM1.
Save.

Lemma OIMs1_is_OIMs1 : (i:V)(ms:Ms)
(Occurs_In_Ms i ms)->
		(Occurs_In_Ms1 i ms)=true.

Cut ((m:M)(oim1_is_oim1 m))/\
	 ((ms:Ms)(oims1_is_oims1 ms)).
Unfold oims1_is_oims1; Intros H; Case H; Auto.
Exact oiM1_is_oiM1.
Save.

Definition oim1_is_oim2 : M->Prop :=
[m:M](i:V)(Occurs_In_M1 i m)=true->
	      (Occurs_In_M i m).

Definition oims1_is_oims2 : Ms->Prop :=
[ms:Ms](i:V)(Occurs_In_Ms1 i ms)=true->
		(Occurs_In_Ms i ms).

Lemma oiM1_is_oiM2 :
	((m:M)(oim1_is_oim2 m))/\
	 ((ms:Ms)(oims1_is_oims2 ms)).

(Apply M_Ms_ind; Unfold oims1_is_oims2 ; Unfold oim1_is_oim2 ).
(Intros v m H i; Rewrite -> OIM1; Intros;
 Cut (or (eq ? (Occurs_In_V1 i v) true) (eq ? (Occurs_In_Ms1 i m) true))).
(Intros c; Case c; Clear  c; Intros).
(Apply Occurs_in_sc1; Apply OIV1_is_OIV2; Auto).

(Apply Occurs_in_sc2; Apply H; Auto).

(Generalize H0 ; Clear  H0; Case (Occurs_In_V1 i v); Auto;
 Case (Occurs_In_Ms1 i m); Auto).

(Intros m H i; Rewrite -> OIM2; Intros; Apply Occurs_in_lambda;
 Apply H; Auto).

(Simpl; Intros; Discriminate H).

(Intros m H m0 H0 i; Rewrite -> OIM4; Intros).
Cut (or (eq ? (Occurs_In_M1 i m) true) (eq ? (Occurs_In_Ms1 i m0) true)).
(Intros c; Case c; Clear  c; Intros).
(Apply Occurs_in_mcons1; Apply H; Auto).

(Apply Occurs_in_mcons2; Apply H0; Auto).

(Generalize H1 ; Clear  H1; Case (Occurs_In_M1 i m); Auto;
 Case (Occurs_In_Ms1 i m0); Auto).
Save.

Lemma OIM1_is_OIM2 : (i:V)(m:M)
	(Occurs_In_M1 i m)=true->
	 (Occurs_In_M i m).

Cut ((m:M)(oim1_is_oim2 m))/\
	 ((ms:Ms)(oims1_is_oims2 ms)).
Unfold oim1_is_oim2.
Intros H.
Case H.
Auto.
Exact oiM1_is_oiM2.
Save.

Lemma OIMs1_is_OIMs2 :
	(i:V)(ms:Ms)
	 (Occurs_In_Ms1 i ms)=true->
	  (Occurs_In_Ms i ms).

Cut ((m:M)(oim1_is_oim2 m))/\
	 ((ms:Ms)(oims1_is_oims2 ms)).
Unfold oims1_is_oims2.
Intros H.
Case H.
Auto.
Exact oiM1_is_oiM2.
Save.

Lemma OIM1_is_OIM3 :
	(i:V)(m:M)
	 ~(Occurs_In_M i m)->
	  (Occurs_In_M1 i m)=false.
Unfold not.
Intros.
Apply bool_dec5.
Unfold not ;Intros;Apply H.
Exact (OIM1_is_OIM2 i m H0).
Save.

Lemma OIMs1_is_OIMs3 :
	(i:V)(ms:Ms)
	 ~(Occurs_In_Ms i ms)->
	  (Occurs_In_Ms1 i ms)=false.

Unfold not.
Intros.
Apply bool_dec5.
(Unfold not ;Intros;Apply H).
Exact (OIMs1_is_OIMs2 i ms H0).
Save.

Lemma OIM1_is_OIM4 :
	(i:V)(m:M)
	 (Occurs_In_M1 i m)=false->
	  ~(Occurs_In_M i m).

Intros.
Cut (not (eq ? (Occurs_In_M1 i m) true)).
Unfold not ;Intros;Apply H0.
Apply OIM1_is_OIM1.
Auto.

Apply bool_dec6.
Auto.
Save.

Lemma OIMs1_is_OIMs4 :
	(i:V)(ms:Ms)
	 (Occurs_In_Ms1 i ms)=false->
	  ~(Occurs_In_Ms i ms).

Intros.
Cut (not (eq ? (Occurs_In_Ms1 i ms) true)).
Unfold not ;Intros;Apply H0.
Apply OIMs1_is_OIMs1.
Auto.

Apply bool_dec6.
Auto.
Save.

Definition OIM_compare : V->M->Prop :=
[i:V][m:M](Occurs_In_M i m)\/~(Occurs_In_M i m).

Lemma OIM_dec :
	(i:V)(m:M)
	 (OIM_compare i m).

(Intros; Unfold OIM_compare ;
 Cut (or (eq ? (Occurs_In_M1 i m) true) (eq ? (Occurs_In_M1 i m) false))).
(Intros c; Case c; Clear  c; Intros).
(Left; Apply OIM1_is_OIM2; Auto).

(Right; Apply OIM1_is_OIM4; Auto).

(Case (Occurs_In_M1 i m); Auto).
Save.

Definition OIMs_compare : V->Ms->Prop :=
[i:V][ms:Ms](Occurs_In_Ms i ms)\/~(Occurs_In_Ms i ms).

Lemma OIMs_dec :
	(i:V)(ms:Ms)
	 (OIMs_compare i ms).

(Intros; Unfold OIMs_compare ;
 Cut (or (eq ? (Occurs_In_Ms1 i ms) true)
       (eq ? (Occurs_In_Ms1 i ms) false))).
(Intros c; Case c; Clear  c; Intros).
(Left; Apply OIMs1_is_OIMs2; Auto).

(Right; Apply OIMs1_is_OIMs4; Auto).

(Case (Occurs_In_Ms1 i ms); Auto).
Save.

Fixpoint
    Occurs_In_N2 [n:N] : V->bool :=
	[i:V]<bool>Case n of
	    (* lam n *)[n':N]
		(Occurs_In_N2 n' (S i))
	    (* an a *)[a:A]
		(Occurs_In_A2 a i)
end with
    Occurs_In_A2 [a:A] : V->bool :=
	[i:V]<bool>Case a of
	    (* ap a n *)[a':A][n:N]
		(orb (Occurs_In_A2 a' i) (Occurs_In_N2 n i))
	    (* var x *)[x:V]
		(Occurs_In_V1 i x)
end.

Definition Occurs_In_N1 : V->N->bool :=
[i:V][n:N](Occurs_In_N2 n i).

Definition Occurs_In_A1 : V->A->bool :=
[i:V][a:A](Occurs_In_A2 a i).

Lemma OIN1 : (i:V)(n:N)
	(Occurs_In_N1 i (lam n))=
	 (Occurs_In_N1 (S i) n).
Auto.
Save.

Lemma OIN2 : (i:V)(a:A)
	(Occurs_In_N1 i (an a))=
	 (Occurs_In_A1 i a).
Auto.
Save.

Lemma OIN3 : (i:V)(a:A)(n:N)
	(Occurs_In_A1 i (ap a n))=
	 (orb (Occurs_In_A1 i a) (Occurs_In_N1 i n)).

Auto.
Save.

Lemma OIN4 : (i,x:V)
	(Occurs_In_A1 i (var x))=
	 (Occurs_In_V1 i x).
Auto.
Save.

Definition oin1_is_oin1 : N->Prop :=
	[n:N](i:V)
	 (Occurs_In_N i n)->
	  (Occurs_In_N1 i n)=true.

Definition oia1_is_oia1 : A->Prop :=
	[a:A](i:V)
	 (Occurs_In_A i a)->
	  (Occurs_In_A1 i a)=true.

Lemma oiN1_is_oiN1 :
	((n:N)(oin1_is_oin1 n))/\
	 ((a:A)(oia1_is_oia1 a)).

(Apply N_A_ind; Unfold oin1_is_oin1 ; Unfold oia1_is_oia1 ; Intros).
Simpl.
(Apply H; Inversion_clear H0; Auto).

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

(Rewrite -> OIN3; Apply ororb; Inversion_clear H1).
(Left; Apply H; Auto).

(Right; Apply H0; Auto).

(Simpl; Inversion_clear H; Apply OIV1_is_OIV1; Auto).
Save.

Lemma OIN1_is_OIN1 :
	(n:N)(i:V)
	 (Occurs_In_N i n)->
	  (Occurs_In_N1 i n)=true.

Cut ((n:N)(oin1_is_oin1 n))/\
	 ((a:A)(oia1_is_oia1 a)).
Intros H; Case H; Auto.
Exact oiN1_is_oiN1.
Save.

Lemma OIA1_is_OIA1 :
	(a:A)(i:V)
	 (Occurs_In_A i a)->
	  (Occurs_In_A1 i a)=true.

Cut ((n:N)(oin1_is_oin1 n))/\
	 ((a:A)(oia1_is_oia1 a)).
Intros H; Case H; Auto.
Exact oiN1_is_oiN1.
Save.

Definition oin1_is_oin2 : N->Prop :=
[n:N](i:V)(Occurs_In_N1 i n)=true->
	      (Occurs_In_N i n).

Definition oia1_is_oia2 : A->Prop :=
[a:A](i:V)(Occurs_In_A1 i a)=true->
	      (Occurs_In_A i a).

Lemma oiN1_is_oiN2 :
	((n:N)(oin1_is_oin2 n))/\
	 ((a:A)(oia1_is_oia2 a)).

(Apply N_A_ind; Unfold oin1_is_oin2 ; Unfold oia1_is_oia2 ).
(Intros n H i; Rewrite -> OIN1; Intros; Apply Occurs_in_lam; Apply H;
 Auto).

(Intros a H i; Rewrite -> OIN2; Intros; Apply Occurs_in_an; Apply H;
 Auto).

(Intros a H n H0 i; Rewrite -> OIN3; Intros;
 Cut (or (eq ? (Occurs_In_A1 i a) true) (eq ? (Occurs_In_N1 i n) true))).
(Intros c; Case c; Clear  c; Intros).
(Apply Occurs_in_ap1; Apply H; Auto).

(Apply Occurs_in_ap2; Apply H0; Auto).

(Generalize H1 ; Clear  H1; Case (Occurs_In_A1 i a); Auto;
 Case (Occurs_In_N1 i n); Auto).

(Intros v i; Rewrite -> OIN4; Intros; Apply Occurs_in_var;
 Apply OIV1_is_OIV2; Auto).
Save.

Lemma OIN1_is_OIN2 :
	(n:N)(i:V)
	 (Occurs_In_N1 i n)=true->
	  (Occurs_In_N i n).

Cut ((n:N)(oin1_is_oin2 n))/\
	 ((a:A)(oia1_is_oia2 a)).
Intros H; Case H; Auto.
Exact oiN1_is_oiN2.
Save.

Lemma OIA1_is_OIA2 :
	(a:A)(i:V)
	 (Occurs_In_A1 i a)=true->
	  (Occurs_In_A i a).

Cut ((n:N)(oin1_is_oin2 n))/\
	 ((a:A)(oia1_is_oia2 a)).
Intros H; Case H; Auto.
Exact oiN1_is_oiN2.
Save.

Lemma OIN1_is_OIN3 :
	(i:V)(n:N)
	 ~(Occurs_In_N i n)->
	  (Occurs_In_N1 i n)=false.

Unfold not; Intros.
Apply bool_dec5.
Unfold not ;Intros;Apply H.
Exact (OIN1_is_OIN2 n i H0).
Save.

Lemma OIA1_is_OIA3 :
	(i:V)(a:A)
	 ~(Occurs_In_A i a)->
	  (Occurs_In_A1 i a)=false.

Unfold not; Intros.
Apply bool_dec5.
Unfold not ;Intros;Apply H.
Exact (OIA1_is_OIA2 a i H0).
Save.

Lemma OIN1_is_OIN4 :
	(i:V)(n:N)
	 (Occurs_In_N1 i n)=false->
	  ~(Occurs_In_N i n).

Intros; Cut (not (eq ? (Occurs_In_N1 i n) true)).
Unfold not ;Intros;Apply H0.
Apply OIN1_is_OIN1.
Auto.

Apply bool_dec6.
Auto.
Save.

Lemma OIA1_is_OIA4 :
	(i:V)(a:A)
	 (Occurs_In_A1 i a)=false->
	  ~(Occurs_In_A i a).

Intros; Cut (not (eq ? (Occurs_In_A1 i a) true)).
Unfold not ;Intros;Apply H0.
Apply OIA1_is_OIA1.
Auto.

Apply bool_dec6.
Auto.
Save.

Definition OIN_compare : V->N->Prop :=
[i:V][n:N](Occurs_In_N i n)\/~(Occurs_In_N i n).

Lemma OIN_dec :
	(i:V)(n:N)
	 (Occurs_In_N i n)\/~(Occurs_In_N i n).

(Intros; Unfold OIN_compare ;
 Cut (or (eq ? (Occurs_In_N1 i n) true) (eq ? (Occurs_In_N1 i n) false))).
(Intros c; Case c; Clear  c; Intros).
(Left; Apply OIN1_is_OIN2; Auto).

(Right; Apply OIN1_is_OIN4; Auto).

(Case (Occurs_In_N1 i n); Auto).
Save.

Definition OIA_compare : V->A->Prop :=
[i:V][a:A](Occurs_In_A i a)\/~(Occurs_In_A i a).

Lemma OIA_dec :
	(i:V)(a:A)
	 (Occurs_In_A i a)\/~(Occurs_In_A i a).

(Intros; Unfold OIA_compare ;
 Cut (or (eq ? (Occurs_In_A1 i a) true) (eq ? (Occurs_In_A1 i a) false))).
(Intros c; Case c; Clear  c; Intros).
(Left; Apply OIA1_is_OIA2; Auto).

(Right; Apply OIA1_is_OIA4; Auto).

(Case (Occurs_In_A1 i a); Auto).
Save.

Lemma NOI_Lift_V_Bridge0 :
	(x,i:V)
	 ~(Occurs_In_V i x)->
	  (lift_V i x)=
	   (lift_V (S i) x).

(Intros j i H; Cut (nat_compare2 i j); Auto; Unfold nat_compare2 ; Intros c; 
 Case c; Clear  c; Intros; Unfold lift_V).
Rewrite -> ltb_is_lt3.
(Rewrite -> ltb_is_lt3; Auto).
Cut (or (eq ? (S i) j) (lt (S i) j)).
(Intros c; Case c; Clear  c; Intros).
(Apply notltii; Auto).

(Apply ltnotlt; Auto).

(Apply lt_S_le; Auto).

(Apply ltnotlt; Auto).

(Case H0; Clear  H0; Intros; Simpl).
(Cut False; Intros).
Contradiction.

(Unfold not  in H; Apply H; Auto).

Rewrite -> (ltb_is_lt1 j i H0).
Rewrite -> ltb_is_lt1.
Auto.

(Apply ltS; Auto).
Save.

Definition NOI_lift_n_bridge0 : N->Prop :=
	[n:N](i:V)
	 ~(Occurs_In_N i n)->
	  (lift_N i n)=
	   (lift_N (S i) n).

Definition NOI_lift_a_bridge0 : A->Prop :=
	[a:A](i:V)
	 ~(Occurs_In_A i a)->
	  (lift_A i a)=
	   (lift_A (S i) a).

Lemma NOI_lift_n_Bridge0 :
	((n:N)(NOI_lift_n_bridge0 n))/\
	 ((a:A)(NOI_lift_a_bridge0 a)).

(Apply N_A_ind; Unfold NOI_lift_n_bridge0 ; Unfold NOI_lift_a_bridge0 ;
 Intros).
(Simpl; Rewrite -> H; Auto).
(Unfold not  in H0; Unfold not ; Intros; Apply H0; Auto).

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

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

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

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

Lemma NOI_Lift_N_Bridge0 : 
	(n:N)(i:V)
	 ~(Occurs_In_N i n)->
	  (lift_N i n)=
	   (lift_N (S i) n).

Cut ((n:N)(NOI_lift_n_bridge0 n))/\
	 ((a:A)(NOI_lift_a_bridge0 a)).
Unfold NOI_lift_n_bridge0.
Intros c; Case c; Clear c; Intros; Auto.
Exact NOI_lift_n_Bridge0.
Save.

Lemma NOI_Lift_A_Bridge0 :
	(a:A)(i:V)
	 ~(Occurs_In_A i a)->
	  (lift_A i a)=
	   (lift_A (S i) a).

Cut ((n:N)(NOI_lift_n_bridge0 n))/\
	 ((a:A)(NOI_lift_a_bridge0 a)).
Unfold NOI_lift_a_bridge0.
Intros c; Case c; Clear c; Intros; Auto.
Exact NOI_lift_n_Bridge0.
Save.

Lemma NOI_Lift_L_Bridge0 :
	(l:L)(i:V)
	 ~(Occurs_In_L i l)->
	  (lift_L i l)=
	   (lift_L (S i) l).

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

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

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

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

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

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

Lemma NOI_Drop_V_Bridge0 :
	(x:V)(i,j:V)
	 (lt i j)->
	  ~(Occurs_In_V (S j) x)->
	   ~(Occurs_In_V j (drop_V i x)).

(Intros n i j H; Unfold drop_V ; Cut (nat_compare2 n i); Auto;
 Unfold nat_compare2 ; Intros c; Case c; Clear  c; Intros c).
(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb ).
Intros.
(Apply OIV1_is_OIV4; Unfold Occurs_In_V1 ).
(Apply nateqb_is_eq3; Apply sym_not_equal; Apply lt_not_eq1;
 Apply lt_trans with j:=i; Auto).

(Case c; Clear  c; Intros).
Rewrite -> ltb_is_lt3.
Unfold Setifb .
(Generalize H ; Clear  H; Rewrite -> H0; Clear  H0; Elim i; Clear  i;
 Intros).
Simpl.
(Inversion_clear H; Auto).
(Apply OIV1_is_OIV4; Unfold Occurs_In_V1 ; Apply nateqb_is_eq3; Auto).

Simpl.
(Apply OIV1_is_OIV4; Unfold Occurs_In_V1 ; Apply nateqb_is_eq3;
 Apply sym_not_equal; Apply lt_not_eq1; Apply Slt; Auto).

(Apply notltii; Auto).

Rewrite -> ltb_is_lt3.
Unfold Setifb .
(Generalize H1 H ; Clear  H1 H; Inversion_clear H0; Intros).
(Simpl; Unfold not ; Intros; Apply H1; Inversion_clear H0; Auto).

(Simpl; Unfold not ; Intros; Apply H1; Inversion_clear H2; Auto).

(Apply ltnotlt; Auto).
Save.

Definition noi_drop_m_bridge0 : M->Prop :=
	[m:M](i,j:V)
         (lt i j)
          ->~(Occurs_In_M (S j) m)
             ->~(Occurs_In_M j (drop_M i m)).

Definition noi_drop_ms_bridge0 : Ms->Prop :=
	[ms:Ms](i,j:V)
         (lt i j)
          ->~(Occurs_In_Ms (S j) ms)
             ->~(Occurs_In_Ms j (drop_Ms i ms)).

Lemma noi_drop_m_Bridge0 :
	((m:M)(noi_drop_m_bridge0 m))/\
	 ((ms:Ms)(noi_drop_ms_bridge0 ms)).

(Apply M_Ms_ind; Unfold noi_drop_m_bridge0 ;
 Unfold noi_drop_ms_bridge0 ; Intros; Auto).
(Apply OIM1_is_OIM4; Rewrite -> DROPM1; Rewrite -> OIM1; Apply ororb1;
 Split).
(Apply OIV1_is_OIV3; Apply NOI_Drop_V_Bridge0; Auto).
(Unfold not ; Intros; Apply H1; Apply Occurs_in_sc1; Auto).

(Apply OIMs1_is_OIMs3; Apply H; Auto).
(Unfold not ; Intros; Apply H1; Apply Occurs_in_sc2; Auto).

(Apply OIM1_is_OIM4; Rewrite -> DROPM2; Rewrite -> OIM2;
 Apply OIM1_is_OIM3; Apply H; Auto; Unfold not ; Intros; Apply H1; 
 Auto).

(Simpl; Unfold not ; Intros; Inversion H1).

(Apply OIMs1_is_OIMs4; Rewrite -> DROPM4; Rewrite -> OIM4;
 Apply ororb1; Split).
(Apply OIM1_is_OIM3; Apply H; Auto; Unfold not ; Intros; Apply H2;
 Apply Occurs_in_mcons1; Auto).

(Apply OIMs1_is_OIMs3; Apply H0; Auto; Unfold not ; Intros; Apply H2;
 Apply Occurs_in_mcons2; Auto).
Save.

Lemma NOI_Drop_M_Bridge0 :
	(m:M)(i,j:V)
         (lt i j)
          ->~(Occurs_In_M (S j) m)
             ->~(Occurs_In_M j (drop_M i m)).

Cut ((m:M)(noi_drop_m_bridge0 m))/\
	 ((ms:Ms)(noi_drop_ms_bridge0 ms)).
Unfold noi_drop_m_bridge0; Intros c; Case c; Clear c; Auto.
Exact noi_drop_m_Bridge0.
Save.

Lemma NOI_Drop_Ms_Bridge0 :
	(ms:Ms)(i,j:V)
         (lt i j)
          ->~(Occurs_In_Ms (S j) ms)
             ->~(Occurs_In_Ms j (drop_Ms i ms)).

Cut ((m:M)(noi_drop_m_bridge0 m))/\
	 ((ms:Ms)(noi_drop_ms_bridge0 ms)).
Unfold noi_drop_ms_bridge0; Intros c; Case c; Clear c; Auto.
Exact noi_drop_m_Bridge0.
Save.

Lemma NOI_Lift_V : (x:V)(i:nat)
	~(Occurs_In_V i (lift_V i x)).

(Intros n i; Unfold lift_V ; Cut (nat_compare2 n i); Auto;
 Unfold nat_compare2 ).
(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 n i d); Unfold Setifb ).
(Apply OIV1_is_OIV4; Unfold Occurs_In_V1 ; Apply nateqb_is_eq3;
 Apply sym_not_equal; Apply lt_not_eq1; Auto).

Rewrite -> ltb_is_lt3.
(Unfold Setifb ; Apply OIV1_is_OIV4; Unfold Occurs_In_V1 ;
 Apply nateqb_is_eq3; Apply lt_not_eq1; Apply ltiSi; Auto).

(Apply notltii; Auto).

Rewrite -> ltb_is_lt3.
(Unfold Setifb ; Apply OIV1_is_OIV4; Unfold Occurs_In_V1 ;
 Apply nateqb_is_eq3; Apply lt_not_eq1; Auto).

(Apply ltnotlt; Auto).
Save.

Lemma NOI_Lift_V2 :(x:V)(i,j:nat)
	~(Occurs_In_V (S i) x)->
	 ~(Occurs_In_V i x)->
	  ~(Occurs_In_V (S i) (lift_V j x)).

(Intros n i j H H0; Unfold lift_V; Cut (nat_compare2 n j); 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 n j d); Simpl; Auto).

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

(Rewrite -> ltb_is_lt3; Auto; Simpl; Unfold not; Intros; Apply H0;
 Inversion_clear H1; Auto).
Save.

Definition noi_lift_m : M->Prop :=
	[m:M](i:nat)
	 ~(Occurs_In_M i (lift_M i m)).

Definition noi_lift_ms : Ms->Prop :=
	[ms:Ms](i:nat)
	 ~(Occurs_In_Ms i (lift_Ms i ms)).

Lemma NOI_lift_m : 
	((m:M)(noi_lift_m m))/\
	 ((ms:Ms)(noi_lift_ms ms)).

(Apply M_Ms_ind; Unfold noi_lift_ms ; Unfold noi_lift_m ; Intros).
(Rewrite -> LIFTM1; Apply OIM1_is_OIM4; Rewrite -> OIM1; Apply ororb1;
 Split).
(Apply OIV1_is_OIV3; Apply NOI_Lift_V).

(Apply OIMs1_is_OIMs3; Apply H).

(Apply OIM1_is_OIM4; Rewrite -> LIFTM2; Rewrite -> OIM2;
 Apply OIM1_is_OIM3; Apply H).

(Apply OIMs1_is_OIMs4; Auto).

(Apply OIMs1_is_OIMs4; Rewrite -> LIFTM4; Rewrite -> OIM4;
 Apply ororb1; Split).
(Apply OIM1_is_OIM3; Auto).

(Apply OIMs1_is_OIMs3; Auto).
Save.

Lemma NOI_Lift_M :
	(m:M)(i:nat)
	 ~(Occurs_In_M i (lift_M i m)).

Cut ((m:M)(noi_lift_m m))/\
	 ((ms:Ms)(noi_lift_ms ms)).
Intros c; Case c; Auto.
Exact NOI_lift_m.
Save.

Lemma NOI_Lift_Ms :
	(ms:Ms)(i:nat)
	 ~(Occurs_In_Ms i (lift_Ms i ms)).
Cut ((m:M)(noi_lift_m m))/\
	 ((ms:Ms)(noi_lift_ms ms)).
Intros c; Case c; Auto.
Exact NOI_lift_m.
Save.

Definition noi_lift_m1 : M->Prop :=
	[m:M](i:nat)(j:nat)
	 ~(Occurs_In_M (S i) m)->
	  ~(Occurs_In_M i m)->
	   ~(Occurs_In_M (S i) (lift_M j m)).

Definition noi_lift_ms1 : Ms->Prop :=
	[ms:Ms](i:nat)(j:nat)
	 ~(Occurs_In_Ms (S i) ms)->
	  ~(Occurs_In_Ms i ms)->
	   ~(Occurs_In_Ms (S i) (lift_Ms j ms)).

Lemma NOI_lift_m1 : 
	((m:M)(noi_lift_m1 m))/\
	 ((ms:Ms)(noi_lift_ms1 ms)).

(Apply M_Ms_ind; Unfold noi_lift_ms1 ; Unfold noi_lift_m1 ; Intros).
(Apply OIM1_is_OIM4; Rewrite -> LIFTM1; Rewrite -> OIM1; Apply ororb1;
 Split).
Cut (not (Occurs_In_V i v)).
Cut (not (Occurs_In_V (S i) v)).
(Intros; Apply OIV1_is_OIV3; Apply NOI_Lift_V2; Auto).

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

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

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

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

(Apply OIM1_is_OIM4; Rewrite -> LIFTM2; Rewrite -> OIM2;
 Apply OIM1_is_OIM3; Apply H).
(Unfold not ; Intros; Apply H0; Auto).

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

(Apply OIMs1_is_OIMs4; Auto).

(Apply OIMs1_is_OIMs4; Rewrite -> LIFTM4; Rewrite -> OIM4;
 Apply ororb1; Split).
(Apply OIM1_is_OIM3; Apply H).
(Unfold not ; Intros; Apply H1; Auto).

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

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

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

Lemma NOI_Lift_M1 :
	(m:M)(i,j:nat)
	 ~(Occurs_In_M (S i) m)->
	  ~(Occurs_In_M i m)->
	   ~(Occurs_In_M (S i) (lift_M j m)).

Cut ((m:M)(noi_lift_m1 m))/\
	 ((ms:Ms)(noi_lift_ms1 ms)).
Intros c; Case c; Auto.
Exact NOI_lift_m1.
Save.

Lemma NOI_Lift_Ms1 :
	(ms:Ms)(i,j:nat)
	 ~(Occurs_In_Ms (S i) ms)->
	  ~(Occurs_In_Ms i ms)->
	   ~(Occurs_In_Ms (S i) (lift_Ms j ms)).

Cut ((m:M)(noi_lift_m1 m))/\
	 ((ms:Ms)(noi_lift_ms1 ms)).
Intros c; Case c; Auto.
Exact NOI_lift_m1.
Save.

Lemma NOI_Lift_L : (l:L)(i:nat)
	~(Occurs_In_L i (lift_L i l)).

(Induction l; Clear  l; Intros; Apply OIL1_is_OIL4; Simpl; Auto).
(Apply OIV1_is_OIV3; Apply NOI_Lift_V; Auto).

(Apply ororb1; Split).
(Apply OIV1_is_OIV3; Apply NOI_Lift_V).

(Apply ororb1; Split; Apply OIL1_is_OIL3).
Apply H.

Apply H0.

(Apply OIL1_is_OIL3; Apply H).
Save.

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

(Intros n i j H H0; Unfold lift_V).
(Cut (nat_compare2 n j); Auto; Unfold nat_compare2; Intros c; Case c;
 Clear  c; Intros).
(Rewrite -> ltb_is_lt1; Auto; Simpl).
(Apply OIV1_is_OIV4; Unfold Occurs_In_V1).
(Apply nateqb_is_eq3; Apply sym_not_equal; Apply lt_not_eq1).
(Apply ltS; Apply lt_trans with j:=j; Auto).

(Case H1; Clear  H1; Intros; Rewrite -> ltb_is_lt3; Auto; Simpl;
 Apply OIV1_is_OIV4; Unfold Occurs_In_V1; Apply nateqb_is_eq3; 
 Auto).
(Rewrite -> H1; Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Unfold not; Intros c; Injection c; Clear  c; Intros; Apply H0; Auto).
Save.

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

Intros.
Rewrite <- H.
Rewrite -> NOI_Lift_V_Bridge0.
Apply NOI_Lift_V.

(Rewrite -> H; Auto).
Save.

Hint OIL_dec.
Hint OIM_dec.
Hint OIMs_dec.
Hint OIN_dec.
Hint OIA_dec.