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))).
Simpl.
Intuition.
Save.

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

Lemma LIFTM3 : (i:nat)(lift_Ms i mnil)=mnil.
Simpl.
Trivial.
Save.

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

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

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

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

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

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

(Unfold V; Intros k i j H; Unfold 2 4 lift_V).
(Cut (nat_compare2 k j); Auto; Unfold nat_compare2; Intros c; Case c;
 Clear  c; Intros).
(Rewrite -> (ltb_is_lt1 k j H0); Simpl).
(Cut (nat_compare2 k i); Auto; Unfold nat_compare2; Intros c; Case c;
 Clear  c; Intros).
(Rewrite -> (ltb_is_lt1 k i H1); Simpl).
(Rewrite -> (ltb_is_lt1 k (S j)); Auto).
Unfold lift_V.
(Rewrite -> (ltb_is_lt1 k i H1); Rewrite -> ltb_is_lt1; Auto).

(Case H1; Clear  H1; Intros).
(Rewrite -> ltb_is_lt3; Auto).
(Simpl; Unfold lift_V; Rewrite -> ltb_is_lt3; Auto).
(Rewrite -> ltb_is_lt1; Auto).

(Rewrite -> ltb_is_lt3; Auto; Simpl; Unfold lift_V;
 Rewrite -> ltb_is_lt3; Auto; Rewrite -> ltb_is_lt1; Auto).

(Case H0; Clear  H0; Intros).
(Repeat (Rewrite -> ltb_is_lt3; Auto); Simpl).
Unfold lift_V.
Repeat (Rewrite -> ltb_is_lt3; Auto).
(Rewrite -> H0; Apply ltnotlt; Auto).

(Rewrite -> H0; Apply ltnotlt; Auto).

(Rewrite -> ltb_is_lt3; Auto; Simpl).
(Rewrite -> ltb_is_lt3; Auto; Simpl; Unfold lift_V).
(Repeat (Rewrite -> ltb_is_lt3; Auto); Simpl).
(Apply ltnotlt; Auto).
(Apply lt_trans with j:=j; Auto).

(Apply ltnotlt; Apply lt_trans with j:=j; Auto).
Save.

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

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

(Simpl; Rewrite -> H; Auto; Rewrite -> H0; Auto).
(Rewrite -> Lift_Lift_V_Bridge; Auto).

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

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

(Apply N_A_ind; Unfold lift_lift_n_bridge ; Unfold lift_lift_a_bridge ;
 Intros).
Simpl.
Rewrite -> H.
Auto.

Auto.

Rewrite -> LIFTN2.
Rewrite -> LIFTN2.
Rewrite -> LIFTN2.
Rewrite -> LIFTN2.
Rewrite -> H.
Auto.

Auto.

Rewrite -> LIFTN3.
Rewrite -> LIFTN3.
Rewrite -> LIFTN3.
Rewrite -> LIFTN3.
Rewrite -> H.
Rewrite -> H0.
Auto.

Auto.

Auto.

Rewrite -> LIFTN4.
Rewrite -> LIFTN4.
Rewrite -> LIFTN4.
Rewrite -> LIFTN4.
Rewrite -> Lift_Lift_V_Bridge.
Auto.

Auto.
Save.

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

Cut ((n:N)(lift_lift_n_bridge n))/\((a:A)(lift_lift_a_bridge a)).
Unfold lift_lift_n_bridge.
Intros H.
Case H.
Auto.
Exact lift_lift_n_Bridge.
Save.

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

Cut ((n:N)(lift_lift_n_bridge n))/\((a:A)(lift_lift_a_bridge a)).
Unfold lift_lift_a_bridge.
Intros H.
Case H.
Auto.
Exact lift_lift_n_Bridge.
Save.

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

(Unfold V; Intros n i j H; Unfold 4 lift_V; Inversion_clear H;
 Clear  i j; Unfold pred).
(Cut (nat_compare2 n i0); Auto; Unfold nat_compare; Intros c; Case c;
 Clear  c; Intros).
(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb; Unfold 2 3 lift_V).
Rewrite -> ltb_is_lt3.
(Unfold Setifb; Unfold lift_V; Rewrite -> ltb_is_lt1; Auto).

(Unfold not; Intros; Inversion H0).

(Case H; Clear  H; Intros).
Rewrite -> ltb_is_lt3.
(Unfold Setifb; Unfold 2 3 lift_V; Rewrite -> ltb_is_lt3).
Rewrite -> ltb_is_lt3.
(Unfold Setifb; Unfold lift_V; Rewrite -> ltb_is_lt3; Auto).

Auto.

(Unfold not; Intros; Inversion H0).

Auto.

(Rewrite -> ltb_is_lt3; Auto).
(Unfold Setifb; Unfold 2 3 lift_V).
Repeat (Rewrite -> ltb_is_lt3; Auto).
(Simpl; Unfold lift_V; Rewrite -> ltb_is_lt3; Auto).

(Unfold not; Intros; Inversion H0).

(Cut (nat_compare2 n j0); Auto; Unfold nat_compare2; Intros c; 
 Case c; Clear  c; Intros).
(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb; Unfold 2 3 lift_V;
 Cut (nat_compare2 n (S i0)); Auto; Unfold nat_compare2; Intros c;
 Case c; Clear  c; Intros).
(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb; Unfold lift_V;
 Rewrite -> ltb_is_lt1; Auto).

(Case H1; Clear  H1; Intros; Rewrite -> ltb_is_lt3; Auto;
 Unfold Setifb; Unfold lift_V; Rewrite -> ltb_is_lt1; Auto).

(Case H; Clear  H; Intros; Rewrite -> ltb_is_lt3; Auto; Simpl;
 Unfold 2 3 lift_V).
(Rewrite -> H; Repeat (Rewrite -> ltb_is_lt3; Auto); Simpl;
 Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).

(Apply lt_not_ltS; Auto).

(Repeat (Rewrite -> ltb_is_lt3; Auto); Simpl; Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).

(Apply ltnotlt; Apply lt_S; Apply lt_trans with j:=j0; Auto).

(Apply ltnotlt; Apply lt_trans1 with j:=j0; Auto).
Save.

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

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

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

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

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

(Apply N_A_ind; Unfold lift_lift_n_bridge0; Unfold lift_lift_a_bridge0;
 Intros).
(Rewrite -> LIFTN1; Rewrite -> LIFTN1; Rewrite -> H; Auto;
 Inversion_clear H0; Auto).

(Rewrite -> LIFTN2; Rewrite -> LIFTN2; Rewrite -> H; Auto).

(Rewrite -> LIFTN3; Rewrite -> LIFTN3; Rewrite -> H; Auto;
 Rewrite -> H0; Auto).

(Rewrite -> LIFTN4; Rewrite -> LIFTN4; Rewrite -> Lift_Lift_V_Bridge0;
 Auto).
Save.

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

Cut ((n:N)(lift_lift_n_bridge0 n))/\((a:A)(lift_lift_a_bridge0 a)).
Unfold lift_lift_n_bridge0; Intros H; Case H; Auto.
Exact lift_lift_n_Bridge0.
Save.

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

Cut ((n:N)(lift_lift_n_bridge0 n))/\((a:A)(lift_lift_a_bridge0 a)).
Unfold lift_lift_a_bridge0; Intros H; Case H; Auto.
Exact lift_lift_n_Bridge0.
Save.

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

(Unfold V; Intros k i j H; Rewrite -> H; Cut (nat_compare2 j k); 
 Auto; Unfold nat_compare2; Intros c; Case c; Clear  c; Intros;
 Unfold 2 4 lift_V).
(Rewrite -> ltb_is_lt3; Auto).
(Simpl; Unfold lift_V; Repeat (Rewrite -> ltb_is_lt3; Auto)).

(Case H0; Clear  H0; Intros).
(Rewrite -> ltb_is_lt3; Auto; Simpl; Unfold lift_V).
Repeat (Rewrite -> ltb_is_lt3; Auto).

(Rewrite -> ltb_is_lt1; Auto; Simpl; Unfold lift_V).
Repeat (Rewrite -> ltb_is_lt1; Auto).
Save.

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

(Apply N_A_ind; Unfold lift_lift_n_bridge1 ;
 Unfold lift_lift_a_bridge1 ; Intros).
(Rewrite -> LIFTN1; Rewrite -> LIFTN1; Rewrite -> LIFTN1;
 Rewrite -> LIFTN1; Rewrite -> H).
Auto.

Auto.

(Rewrite -> LIFTN2; Rewrite -> LIFTN2; Rewrite -> LIFTN2;
 Rewrite -> LIFTN2; Rewrite -> H; Auto).

(Rewrite -> LIFTN3; Rewrite -> LIFTN3; Rewrite -> LIFTN3;
 Rewrite -> LIFTN3; Rewrite -> H).
Rewrite -> H0.
Auto.

Auto.

Auto.

(Rewrite -> LIFTN4; Rewrite -> LIFTN4; Rewrite -> Lift_Lift_V_Bridge1;
 Auto).
Save.

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

Cut ((n:N)(lift_lift_n_bridge1 n))/\((a:A)(lift_lift_a_bridge1 a)).
Unfold lift_lift_n_bridge1.
Intros c.
Case c.
Intros.
Auto.
Exact lift_lift_n_Bridge1.
Save.

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

Cut ((n:N)(lift_lift_n_bridge1 n))/\((a:A)(lift_lift_a_bridge1 a)).
Unfold lift_lift_a_bridge1.
Intros c.
Case c.
Intros.
Auto.
Exact lift_lift_n_Bridge1.
Save.

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

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

(Simpl; Rewrite -> H; Auto; Rewrite -> H0; Auto;
 Rewrite -> Lift_Lift_V_Bridge1; Auto).

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