Require MinMJ_LMN.

Recursive Definition lift_V : nat->V->V :=
i j => (Setifb V (ltb j i) j (S j)).

Recursive Definition
    lift_L : nat->L->L :=
	i (vr x) => (vr (lift_V i x)) |
	i (app x l1 l2) =>
		(app (lift_V i x) (lift_L i l1) (lift_L (S i) l2)) |
	i (lm l) => (lm (lift_L (S i) l)).

Fixpoint
    lift_M1 [m:M] : nat->M :=
	[i:nat]<M>Case m of
	    (* x;ms *)[x:V][ms:Ms]
		(sc (lift_V i x) (lift_Ms1 ms i))
	    (* lam m *)[m':M]
		(lambda (lift_M1 m' (S i)))
end with
    lift_Ms1 [ms:Ms] : nat->Ms :=
	[i:nat]<Ms>Case ms of
	    (* mnil *)
		mnil
	    (* m::ms *)[m:M][ms':Ms]
		(mcons (lift_M1 m i) (lift_Ms1 ms' i))
end.

Recursive Definition
    lift_M : nat->M->M :=
	i m => (lift_M1 m i).

Recursive Definition
    lift_Ms : nat->Ms->Ms :=
	i ms => (lift_Ms1 ms i).

Fixpoint
    lift_N1 [n:N] : nat->N :=
	[i:nat]<N>Case n of
	    (* lam n *)[n':N]
		(lam (lift_N1 n' (S i)))
	    (* an a *)[a:A]
		(an (lift_A1 a i))
end with
    lift_A1 [a:A] : nat->A :=
	[i:nat]<A>Case a of
	    (* ap a n *)[a':A][n:N]
		(ap (lift_A1 a' i) (lift_N1 n i))
	    (* var x *)[x:V]
		(var (lift_V i x))
end.

Recursive Definition lift_N : nat->N->N :=
i n => (lift_N1 n i).

Recursive Definition lift_A : nat->A->A :=
i a => (lift_A1 a i).

Lemma LIFTM1 : (i:nat)(x:V)(ms:Ms)
	((lift_M i (sc x ms)) =
	 (sc (lift_V i x) (lift_Ms i ms))).

Lemma LIFTM2 : (i:nat)(m:M)((lift_M i (lambda m)) = (lambda (lift_M (S i) m))).

Lemma LIFTM3 : (i:nat)(lift_Ms i mnil)=mnil.

Lemma LIFTM4 : (i:nat)(m:M)(ms:Ms)((lift_Ms i (mcons m ms)) = 
			    (mcons (lift_M i m) (lift_Ms i ms))).

Lemma LIFTN1 : (i:nat)(n:N)((lift_N i (lam n)) = (lam (lift_N (S i) n))).

Lemma LIFTN2 : (i:nat)(a:A)((lift_N i (an a)) = (an (lift_A i a))).

Lemma LIFTN3 : (i:nat)(a:A)(n:N)
	((lift_A i (ap a n)) = (ap (lift_A i a) (lift_N i n))).

Lemma LIFTN4 : (i:nat)(x:V)((lift_A i (var x)) = (var (lift_V i x))).

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

Lemma Lift_Lift_L_Bridge : (l:L)(i,j:nat)
	(lt i j)->
	 (lift_L i (lift_L j l))=
	  (lift_L (S j) (lift_L i l)).

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

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

Lemma lift_lift_n_Bridge : 
	((n:N)(lift_lift_n_bridge n))/\
	 ((a:A)(lift_lift_a_bridge a)).

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

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

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

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

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

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

Lemma lift_lift_n_Bridge0 : 
	((n:N)(lift_lift_n_bridge0 n))/\
	 ((a:A)(lift_lift_a_bridge0 a)).

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

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

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

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

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

Lemma lift_lift_n_Bridge1 : 
	((n:N)(lift_lift_n_bridge1 n))/\((a:A)(lift_lift_a_bridge1 a)).

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

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

Lemma Lift_Lift_L_Bridge1 :(l:L)(i,j:nat)
	 i=j->
	  (lift_L i (lift_L j l))=(lift_L (S j) (lift_L i l)).