Require MinMJ_Occurs_Lift.

Recursive Definition
    lifts_V : nat->nat->V->V :=
	O j x => x |
	(S i) j x => (lift_V j (lifts_V i j x)).

Recursive Definition
    lifts_L : nat->nat->L->L :=
	i j (vr x) => (vr (lifts_V i j x)) |
	i j (app x l l0) =>
		(app (lifts_V i j x) (lifts_L i j l) (lifts_L i (S j) l0)) |
	i j (lm l) => (lm (lifts_L i (S j) l)).

Fixpoint
    lifts_M1 [m:M] : nat->nat->M :=
	[i,j:nat]
	<M>Case m of
	    (* x;ms *)[x:V][ms:Ms]
		(sc (lifts_V i j x) (lifts_Ms1 ms i j))
	    (* \m *)[m:M]
		(lambda (lifts_M1 m i (S j)))
	end
with
    lifts_Ms1 [ms:Ms] : nat->nat->Ms :=
	[i,j:nat]
	<Ms>Case ms of
	    (* mnil *)mnil
	    (* m::ms *)[m:M][ms:Ms]
		(mcons (lifts_M1 m i j) (lifts_Ms1 ms i j))
	end.

Recursive Definition lifts_M : nat->nat->M->M :=
i j m => (lifts_M1 m i j).

Recursive Definition lifts_Ms : nat->nat->Ms->Ms :=
i j ms => (lifts_Ms1 ms i j).

Lemma LIFTSM1 : (i,j:nat)(x:V)(ms:Ms)
	(lifts_M i j (sc x ms))=
	 (sc (lifts_V i j x) (lifts_Ms i j ms)).

Lemma LIFTSM2 : (i,j:nat)(m:M)
	(lifts_M i j (lambda m))=
	 (lambda (lifts_M i (S j) m)).

Lemma LIFTSM3 : (i,j:nat)
	(lifts_Ms i j mnil)=mnil.

Lemma LIFTSM4 : (i,j:nat)(m:M)(ms:Ms)
	(lifts_Ms i j (mcons m ms))=
	 (mcons (lifts_M i j m) (lifts_Ms i j ms)).

Lemma Lifts_L0 : (l:L)(j:nat)
	(lifts_L O j l)=l.

Definition lifts_m0 : M->Prop :=
	[m:M](j:nat)
	 (lifts_M O j m)=m.

Definition lifts_ms0 : Ms->Prop :=
	[ms:Ms](j:nat)
	 (lifts_Ms O j ms)=ms.

Lemma Lifts_m0 :
	((m:M)(lifts_m0 m))/\
	 ((ms:Ms)(lifts_ms0 ms)).

Lemma Lifts_M0 :
	(m:M)(j:nat)
	 (lifts_M O j m)=m.

Lemma Lifts_Ms0 :
	(ms:Ms)(j:nat)
	 (lifts_Ms O j ms)=ms.

Lemma Lifts_L_rec1 : (l:L)(i,j:nat)
	(lifts_L (S i) j l)=(lift_L j (lifts_L i j l)).

Definition lifts_m_rec1 : M->Prop :=
	[m:M](i,j:nat)
	 (lifts_M (S i) j m)=(lift_M j (lifts_M i j m)).

Definition lifts_ms_rec1 : Ms->Prop :=
	[ms:Ms](i,j:nat)
	 (lifts_Ms (S i) j ms)=(lift_Ms j (lifts_Ms i j ms)).

Lemma Lifts_m_rec1 :
	((m:M)(lifts_m_rec1 m))/\
	 ((ms:Ms)(lifts_ms_rec1 ms)).

Lemma Lifts_M_rec1 :
	(m:M)(i,j:nat)
	 (lifts_M (S i) j m)=(lift_M j (lifts_M i j m)).

Lemma Lifts_Ms_rec1 :
	(ms:Ms)(i,j:nat)
	 (lifts_Ms (S i) j ms)=(lift_Ms j (lifts_Ms i j ms)).

Lemma Lifts_V_rec2 :
	(x:V)(i,j:nat)
	 (lifts_V (S i) j x)=
	  (lifts_V i j (lift_V j x)).

Lemma Lifts_L_rec2 :
	(l:L)(i,j:nat)
	 (lifts_L (S i) j l)=
	  (lifts_L i j (lift_L j l)).

Definition lifts_m_rec2 : M->Prop :=
	[m:M](i,j:nat)
	 (lifts_M (S i) j m)=(lifts_M i j (lift_M j m)).

Definition lifts_ms_rec2 : Ms->Prop :=
	[ms:Ms](i,j:nat)
	 (lifts_Ms (S i) j ms)=(lifts_Ms i j (lift_Ms j ms)).

Lemma Lifts_m_rec2 :
	((m:M)(lifts_m_rec2 m))/\
	 ((ms:Ms)(lifts_ms_rec2 ms)).

Lemma Lifts_M_rec2 :
	(m:M)(i,j:nat)
	 (lifts_M (S i) j m)=(lifts_M i j (lift_M j m)).

Lemma Lifts_Ms_rec2 :
	(ms:Ms)(i,j:nat)
	 (lifts_Ms (S i) j ms)=(lifts_Ms i j (lift_Ms j ms)).

Lemma Lifts_Msub_Bridge0 :
	(k:nat)(x:V)(m,m0:M)(i,j:nat)
	 (lt i j)->
	  (lifts_M k j (MsubstVMV x m0 i m))=
	   (MsubstVMV (lifts_V k j x) (lifts_M k j m0) i (lifts_M k (S j) m)).

Lemma Lifts_Mssub_Bridge0 :
	(k:nat)(x:V)(ms:Ms)(m0:M)(i,j:nat)
	 (lt i j)->
	  (lifts_Ms k j (MssubstVMV x m0 i ms))=
	   (MssubstVMV (lifts_V k j x)
		       (lifts_M k j m0)
		       i
		       (lifts_Ms k (S j) ms)).

Lemma Lifts_Msub_Bridge1 :
	(k:nat)(x:V)(m,m0:M)(i,j:nat)
	 i=j->
	  (lifts_M k j (MsubstVMV x m0 i m))=
	   (MsubstVMV (lifts_V k j x) (lifts_M k j m0) i (lifts_M k (S j) m)).

Lemma Lifts_Mssub_Bridge1 :
	(k:nat)(x:V)(ms:Ms)(m0:M)(i,j:nat)
	 i=j->
	  (lifts_Ms k j (MssubstVMV x m0 i ms))=
	   (MssubstVMV (lifts_V k j x)
		       (lifts_M k j m0)
		       i
		       (lifts_Ms k (S j) ms)).

Lemma Lifts_PhiBar_Bridge : (l:L)(i,j:nat)
	(lifts_M i j (phibar l))=
	 (phibar (lifts_L i j l)).

Lemma Lifts_Lift_V_Bridge3 :
	(x:V)(i,j,k:nat)
	 ~(lt k j)->
	   (lifts_V i j (lift_V k x))=
	    (lift_V (plus i k) (lifts_V i j x)).

Lemma Lifts_Lift_L_Bridge3 :
	(l:L)(i,j,k:nat)
	 ~(lt k j)->
	   (lifts_L i j (lift_L k l))=
	    (lift_L (plus i k) (lifts_L i j l)).

Lemma Lifts_Lifts_L_Bridge0 :
	(i,j,k,n:nat)(l:L)
	 k=n->
	  (lifts_L i k (lifts_L j n l))=
	   (lifts_L (plus i j) n l).