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

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.

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

Lemma OIV1_is_OIV3 : (i:V)(x:V)
		~(Occurs_In_V i x)->
		 (Occurs_In_V1 i x)=false.

Lemma OIV1_is_OIV4 : (i:V)(x:V)
		(Occurs_In_V1 i x)=false->
		 ~(Occurs_In_V i x).

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

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.

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

Lemma OIL1_is_OIL3 :
	(l:L)(i:V)
	 ~(Occurs_In_L i l)->
	  (Occurs_In_L1 i l)=false.

Lemma OIL1_is_OIL4 :
	(l:L)(i:V)
	 (Occurs_In_L1 i l)=false->
	  ~(Occurs_In_L i l).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma NOI_Lift_Ms :
	(ms:Ms)(i:nat)
	 ~(Occurs_In_Ms i (lift_Ms i ms)).

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

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

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

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

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

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