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

Auto.
Save.

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

Auto.
Save.

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

Auto.
Save.

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

Auto.
Save.

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

Induction l; Clear l; Intros; Auto.

Rewrite lifts_L_eq2; Unfold lifts_V; Rewrite H; Rewrite H0; Auto.

Rewrite lifts_L_eq3; Rewrite H; Auto.
Save.

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

Apply M_Ms_ind; Unfold lifts_m0; Unfold lifts_ms0; Intros; Auto.

Rewrite LIFTSM1; Unfold lifts_V; Rewrite H; Auto.

Rewrite LIFTSM2; Rewrite H; Auto.

Rewrite LIFTSM4; Rewrite H; Rewrite H0; Auto.
Save.

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

Cut ((m:M)(lifts_m0 m))/\
	 ((ms:Ms)(lifts_ms0 ms)).
Intros c; Case c; Auto.
Exact Lifts_m0.
Save.

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

Cut ((m:M)(lifts_m0 m))/\
	 ((ms:Ms)(lifts_ms0 ms)).
Intros c; Case c; Auto.
Exact Lifts_m0.
Save.

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

Induction l; Clear l; Intros; Auto.

Rewrite lifts_L_eq2; Unfold lifts_V; Rewrite H; Rewrite H0; Auto.

Rewrite lifts_L_eq3; Rewrite H; Auto.
Save.

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

Apply M_Ms_ind; Unfold lifts_m_rec1; Unfold lifts_ms_rec1; Intros; Auto.

Rewrite LIFTSM1; Unfold lifts_V; Rewrite H; Auto.

Rewrite LIFTSM2; Rewrite H; Auto.

Rewrite LIFTSM4; Rewrite H; Rewrite H0; Auto.
Save.

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

Cut ((m:M)(lifts_m_rec1 m))/\
	 ((ms:Ms)(lifts_ms_rec1 ms)).
Intros c; Case c; Auto.
Exact Lifts_m_rec1.
Save.

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

Cut ((m:M)(lifts_m_rec1 m))/\
	 ((ms:Ms)(lifts_ms_rec1 ms)).
Intros c; Case c; Auto.
Exact Lifts_m_rec1.
Save.

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

(Induction i; Clear  i; Intros; Auto; Rewrite -> lifts_V_eq2;
 Rewrite -> H; Auto).
Save.

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

(Induction l; Clear  l; Intros; Auto).
(Rewrite -> lifts_L_eq1; Rewrite -> lift_L_eq1; Rewrite -> lifts_L_eq1;
 Rewrite -> Lifts_V_rec2; Auto).

(Rewrite -> lifts_L_eq2; Rewrite -> lift_L_eq2; Rewrite -> lifts_L_eq2;
 Rewrite -> Lifts_V_rec2; Rewrite -> H; Rewrite -> H0; Auto).

(Rewrite -> lifts_L_eq3; Rewrite -> lift_L_eq3; Rewrite -> lifts_L_eq3;
 Rewrite -> H; Auto).
Save.

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

Apply M_Ms_ind; Unfold lifts_m_rec2; Unfold lifts_ms_rec2; Intros; Auto.

Rewrite LIFTSM1; Rewrite Lifts_V_rec2; Rewrite H; Auto.

Rewrite LIFTSM2; Rewrite H; Auto.

Rewrite LIFTSM4; Rewrite H; Rewrite H0; Auto.
Save.

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

Cut ((m:M)(lifts_m_rec2 m))/\
	 ((ms:Ms)(lifts_ms_rec2 ms)).
Intros c; Case c; Auto.
Exact Lifts_m_rec2.
Save.

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

Cut ((m:M)(lifts_m_rec2 m))/\
	 ((ms:Ms)(lifts_ms_rec2 ms)).
Intros c; Case c; Auto.
Exact Lifts_m_rec2.
Save.

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

(Induction k; Clear  k; Intros).
(Rewrite -> Lifts_M0; Unfold lifts_V ; Rewrite -> Lifts_M0;
 Rewrite -> Lifts_M0; Auto).

(Rewrite -> Lifts_M_rec2; Rewrite -> Lift_Msub_Bridge0; Auto;
 Rewrite -> H;  Auto; Rewrite -> Lifts_V_rec2; Rewrite -> Lifts_M_rec2;
 Rewrite -> Lifts_M_rec2; Auto).
Save.

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

(Induction ms; Clear  ms; Intros; Auto; Rewrite -> MSVMV4;
 Rewrite -> LIFTSM4; Rewrite -> H; Auto;
 Rewrite -> Lifts_Msub_Bridge0; Auto).
Save.

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

(Induction k; Clear  k; Intros).
(Rewrite -> Lifts_M0; Unfold lifts_V ; Rewrite -> Lifts_M0;
 Rewrite -> Lifts_M0; Auto).

(Rewrite -> Lifts_M_rec2; Rewrite -> Lift_Msub_Bridge1; Auto;
 Rewrite -> H;  Auto; Rewrite -> Lifts_V_rec2; Rewrite -> Lifts_M_rec2;
 Rewrite -> Lifts_M_rec2; Auto).
Save.

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

(Induction ms; Clear  ms; Intros; Auto; Rewrite -> MSVMV4;
 Rewrite -> LIFTSM4; Rewrite -> H; Auto;
 Rewrite -> Lifts_Msub_Bridge1; Auto).
Save.

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

(Induction l; Clear  l; Intros; Auto).
Rewrite -> phibar_eq2.
(Elim j; Clear  j; Intros).
Rewrite -> Lifts_Msub_Bridge1; Auto.
Rewrite -> lifts_L_eq2.
Rewrite -> phibar_eq2.
(Rewrite -> H; Auto; Rewrite -> H0; Auto).

(Rewrite -> Lifts_Msub_Bridge0; Auto).
(Rewrite -> lifts_L_eq2; Rewrite -> phibar_eq2; Rewrite -> H; Auto).
(Rewrite -> H0; Auto).

(Rewrite -> phibar_eq3; Rewrite -> LIFTSM2; Rewrite -> H; Auto).
Save.

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

(Intros n i; Generalize n ; Elim i; Clear  n i; Intros).
(Unfold lifts_V ; Unfold plus ; Auto).

(Rewrite -> lifts_V_eq2; Rewrite -> lifts_V_eq2).
(Rewrite -> plus_eq2; Rewrite -> H).
Cut (or (eq ? k j) (lt j k)).
(Clear  H0; Intros H0; Case H0; Clear  H0; Intros).
(Rewrite -> H0; Clear  H0 k).
Rewrite -> (Lift_Lift_V_Bridge0 (lifts_V n j n0) (S (plus n j))).
(Unfold pred ; Auto).

(Apply ltSplus2; Auto).

Rewrite -> (Lift_Lift_V_Bridge0 (lifts_V n j n0) (S (plus n k))).
(Unfold pred ; Auto).

(Apply ltSplus3; Auto).

(Apply not_lt_eq_lt; Auto).

Auto.
Save.

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

(Induction l; Clear  l; Intros; Auto).
(Rewrite -> lift_L_eq1; Rewrite -> lifts_L_eq1;
 Rewrite -> Lifts_Lift_V_Bridge3; Auto).

(Rewrite -> lift_L_eq2; Rewrite -> lifts_L_eq2;
 Rewrite -> Lifts_Lift_V_Bridge3; Auto; Rewrite -> H; Auto;
 Rewrite -> H0; Auto).
(Rewrite -> (sym_plus i (S k)); Rewrite -> plus_eq2;
 Rewrite -> (sym_plus k i); Auto).

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

(Rewrite -> lift_L_eq3; Rewrite -> lifts_L_eq3; Rewrite -> H; Auto).
(Rewrite -> sym_plus; Rewrite -> plus_eq2; Rewrite -> sym_plus; Auto).

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

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

(Induction i; Clear  i; Intros; Auto).
(Rewrite -> Lifts_L0; Auto).

(Rewrite -> Lifts_L_rec1; Rewrite -> H; Auto; Rewrite -> H0;
 Rewrite -> plus_eq2; Rewrite -> Lifts_L_rec1; Auto).
Save.