Require Export MinMJ_PermDef.
Require Export MinMJ_Normal_RhoBar.
Require Export MinMJ_Strength.
Require Export MinMJ_Bridge3.

Inductive
    L_Permn : L->L->Prop :=
	l_permn_base : 
	    (l0,l1:L)
	       l0=l1->
	        (L_Permn l0 l1) |
	l_permn_rec :
	    (l0,l1,l2:L)
	     (L_Perm1 l0 l1)->
	      (L_Permn l1 l2)->
	       (L_Permn l0 l2).

Scheme L_Permn_ind1 := Induction for L_Permn Sort Prop.

Hint l_permn_base.

Definition l_admis_perm1 :
	(l,l0:L)(L_Perm1 l l0)->Prop :=
	 [l,l0:L][d:(L_Perm1 l l0)]
	   (h:Hyps)(P:F)(L_Deriv h l P)->
	    (L_Deriv h l0 P).

Lemma L_admis_perm1 :
	(l,l0:L)(D:(L_Perm1 l l0))
	 (l_admis_perm1 l l0 D).

(Intros; Apply L_Perm1_ind1; Clear  D l l0; Unfold l_admis_perm1;
 Intros; Auto).
(Inversion_clear H0; Apply Implies_R; Apply H; Auto).

(Inversion_clear H0; Apply Implies_L with P:=P0 Q:=Q; Auto).

(Inversion_clear H0; Apply Implies_L with P:=P0 Q:=Q; Auto).

(Inversion_clear H; Rewrite <- (Strengthen_Hyps_eq2 Q h);
 Apply L_Admis_Strengthen; Auto).

(Inversion_clear H; Inversion_clear H2; Inversion_clear H).
(Apply Implies_L with P:=P1 Q:=Q0; Auto).
(Apply Implies_L with P:=P0 Q:=Q; Auto).

(Apply Implies_L with P:=P0 Q:=Q; Auto).
(Rewrite <- Weaken_Hyps_eq1; Apply In_Weaken_Hyps; Auto).

(Apply L_Admis_Weaken_Top; Auto).

(Apply L_Admis_Exch_Top; Auto).

(Inversion_clear H; Inversion_clear H2).
(Generalize H0 H3 H4 ; Clear  H0 H3 H4; Inversion_clear H; Intros).
(Apply Implies_L with P:=P0 Q:=(Impl P1 Q0); Auto).
(Apply Implies_L with P:=P1 Q:=Q0; Auto).
(Apply Implies_L with P:=P0 Q:=(Impl P1 Q0); Auto).
(Rewrite <- Weaken_Hyps_eq1; Apply In_Weaken_Hyps; Auto).

(Apply L_Admis_Weaken_Top; Auto).

(Rewrite <- (Weaken_Hyps_eq1 (Impl P1 Q0) h);
 Rewrite <- Weaken_Hyps_eq3).
(Apply L_Admis_Weaken; Simpl; Auto).

(Apply Implies_L with P:=P0 Q:=(Impl P1 Q0); Auto).
Simpl.
(Rewrite <- Weaken_Hyps_eq1; Apply In_Weaken_Hyps; Auto;
 Rewrite <- Weaken_Hyps_eq1; Apply In_Weaken_Hyps; Auto).

(Rewrite -> Lifts_L_rec1; Rewrite -> Lifts_L_rec1; Rewrite -> Lifts_L0;
 Apply L_Admis_Weaken_Top; Apply L_Admis_Weaken_Top; Auto).

Apply L_Admis_Exch_Top.
(Rewrite <- (Weaken_Hyps_eq1 (Impl P1 Q0) h);
 Rewrite <- Weaken_Hyps_eq3; Rewrite <- Weaken_Hyps_eq3;
 Apply L_Admis_Weaken; Simpl; Auto).

Inversion_clear H.
(Generalize H0 H1 ; Clear  H0 H1; Inversion_clear H2; Intros).
(Apply Implies_R; Auto).
(Apply Implies_L with P:=P0 Q:=Q; Auto).
(Rewrite <- Weaken_Hyps_eq1; Apply In_Weaken_Hyps; Auto).

(Apply L_Admis_Weaken_Top; Auto).

(Apply L_Admis_Exch_Top; Auto).
Save.

Lemma L_Admis_Perm1 :
	(l,l0:L)(h:Hyps)(P:F)
	 (L_Perm1 l l0)->
	  (L_Deriv h l P)->
	   (L_Deriv h l0 P).

Cut (l,l0:L)(D:(L_Perm1 l l0))(l_admis_perm1 l l0 D).
(Unfold l_admis_perm1; Intros).
Exact (H l l0 H0 h P H1).

Exact L_admis_perm1.
Save.

Lemma L_Perm1n :
	(l,l0:L)
	 (L_Perm1 l l0)->
	  (L_Permn l l0).

(Intros; Apply l_permn_rec with l1:=l0; Auto).
Save.

Definition l_permnn : (l,l0:L)(L_Permn l l0)->Prop :=
	[l,l0:L][d:(L_Permn l l0)]
	 (l1:L)
	  (L_Permn l0 l1)->
	   (L_Permn l l1).

Lemma L_permnn :
	(l,l0:L)(d:(L_Permn l l0))
	 (l_permnn l l0 d).

(Intros; Apply L_Permn_ind1; Unfold l_permnn; Clear  d l l0;
 Intros; Auto).
(Rewrite -> e; Auto).

(Apply l_permn_rec with l1:=l1; Auto).
Save.

Lemma L_Permnn :
	(l,l0,l1:L)
	 (L_Permn l l0)->
	  (L_Permn l0 l1)->
	   (L_Permn l l1).

Cut (l,l0:L)(d:(L_Permn l l0))(l_permnn l l0 d).
(Unfold l_permnn; Intros).
(Apply (H l l0); Auto).

Exact L_permnn.
Save.

Definition l_permn_app1 :
	(l,l0:L)(L_Permn l l0)->Prop :=
	 [l,l0:L][D:(L_Permn l l0)]
	  (x:V)(l1:L)
	   (L_Permn (app x l l1) (app x l0 l1)).

Lemma L_permn_app1 :
	(l,l0:L)(D:(L_Permn l l0))
	 (l_permn_app1 l l0 D).

(Intros; Apply L_Permn_ind1; Clear  D l l0; Unfold l_permn_app1;
 Intros; Auto).
(Rewrite -> e; Auto).

Apply l_permn_rec with l1:=(app x l1 l4).
(Apply l_perm1_app1; Auto).

(Apply H; Auto).
Save.

Lemma L_Permn_app1 :
	(l,l0,l1:L)(x:V)
	 (L_Permn l l0)->
	  (L_Permn (app x l l1) (app x l0 l1)).

Cut (l,l0:L)(d:(L_Permn l l0))(l_permn_app1 l l0 d).
(Unfold l_permn_app1; Intros).
Exact (H l l0 H0 x l1).

Exact L_permn_app1.
Save.

Definition l_permn_app2 :
	(l0,l1:L)(L_Permn l0 l1)->Prop :=
	 [l0,l1:L][D:(L_Permn l0 l1)]
	  (x:V)(l:L)
	   (L_Permn (app x l l0) (app x l l1)).

Lemma L_permn_app2 :
	(l0,l1:L)(D:(L_Permn l0 l1))
	 (l_permn_app2 l0 l1 D).

(Intros; Apply L_Permn_ind1; Clear  D l0 l1; Unfold l_permn_app2;
 Intros; Auto).
(Rewrite -> e; Auto).

Apply l_permn_rec with l1:=(app x l4 l1).
(Apply l_perm1_app2; Auto).

(Apply H; Auto).
Save.

Lemma L_Permn_app2 :
	(l,l0,l1:L)(x:V)
	 (L_Permn l0 l1)->
	  (L_Permn (app x l l0) (app x l l1)).

Cut (l0,l1:L)(D:(L_Permn l0 l1))(l_permn_app2 l0 l1 D).
(Unfold l_permn_app2; Intros).
Exact (H l0 l1 H0 x l).

Exact L_permn_app2.
Save.

Lemma L_Permn_app :
	(x:V)(l0,l1,l2,l3:L)
	 (L_Permn l0 l1)->
	   (L_Permn l2 l3)->
	    (L_Permn (app x l0 l2) (app x l1 l3)).

Intros.
Apply L_Permnn with l0:=(app x l1 l2).
(Apply L_Permn_app1; Auto).

(Apply L_Permn_app2; Auto).
Save.

Definition l_permn_lm :
	(l0,l1:L)(L_Permn l0 l1)->Prop :=
	 [l0,l1:L][d:(L_Permn l0 l1)]
	    (L_Permn (lm l0) (lm l1)).

Lemma L_permn_lm :
	(l0,l1:L)(d:(L_Permn l0 l1))
	 (l_permn_lm l0 l1 d). 

(Intros; Apply L_Permn_ind1; Unfold l_permn_lm; Clear  d l0 l1; 
 Intros; Auto).
(Rewrite -> e; Auto).

(Apply l_permn_rec with l1:=(lm l1); Auto).
(Apply l_perm1_lm; Auto).
Save.

Lemma L_Permn_lm :
	(l,l0:L)
	 (L_Permn l l0)->
	  (L_Permn (lm l) (lm l0)).

Cut (l0,l1:L)(d:(L_Permn l0 l1))(l_permn_lm l0 l1 d).
(Unfold l_permn_lm; Intros).
Exact (H l l0 H0).

Exact L_permn_lm.
Save.

Definition l_admis_permn :
	(l,l0:L)(L_Permn l l0)->Prop :=
	 [l,l0:L][d:(L_Permn l l0)]
	  (h:Hyps)(P:F)
	   (L_Deriv h l P)->
	    (L_Deriv h l0 P).

Lemma L_admis_permn :
	(l,l0:L)(d:(L_Permn l l0))
	 (l_admis_permn l l0 d).

(Intros; Apply L_Permn_ind1; Unfold l_admis_permn; Clear  d l l0;
 Intros; Auto).
(Rewrite <- e; Auto).

Apply H.
(Apply L_Admis_Perm1 with l:=l0; Auto).
Save.

Lemma L_Admis_Permn :
	(h:Hyps)(l0,l1:L)(P:F)
	 (L_Permn l0 l1)->
	  (L_Deriv h l0 P)->
	   (L_Deriv h l1 P).

Cut (l0,l1:L)(d:(L_Permn l0 l1))(l_admis_permn l0 l1 d).
(Unfold l_admis_permn; Intros).
Exact (H l0 l1 H0 h P H1).

Exact L_admis_permn.
Save.

(*
Definition hv_rhobar_m : M->Prop :=
	[m:M](x:V)(l1,l2:L)
	(rhobar m)=(app x l1 l2)->
	 (HV_L l2)=O.

Definition hv_rhobar_ms : Ms->Prop :=
	[ms:Ms]
	 (HV_L (rhobar (sc O ms)))=O.

Lemma HV_rhobar_m :
	((m:M)(hv_rhobar_m m))/\
	 ((ms:Ms)(hv_rhobar_ms ms)).

Apply M_Ms_Height_ind.
(Destruct m; Clear  m).
(Intros x ms; Generalize x ; Case ms; Clear  x ms; Unfold hv_rhobar_m;
 Unfold hv_rhobar_ms; Intros).
(Case H; Clear  H; Intros).
(Simpl in H0; Discriminate H0).

(Generalize H0 ; Clear  H0; Rewrite -> RhoBar2; Intros;
 Injection H0; Clear  H0; Intros).
Rewrite <- H0.
(Case H; Clear  H; Intros).
(Apply H3; Auto).
(Rewrite -> Height_Lift_Ms; Rewrite -> HTM1; Rewrite -> HTM4;
 Rewrite -> sym_max_nat; Apply ltS; Apply lt_max_nat1; Auto).

(Unfold hv_rhobar_m; Unfold hv_rhobar_ms; Intros).
(Simpl in H0; Discriminate H0).

(Destruct ms; Clear  ms; Unfold hv_rhobar_ms; Unfold hv_rhobar_m;
 Intros).
Auto.

Rewrite -> RhoBar2.
Rewrite -> HV_L_eq2.
(Case H; Clear  H; Intros).
(Rewrite -> H; Auto).
(Rewrite -> Height_Lift_Ms; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Apply lt_max_nat1; Auto).
Save.

Lemma HV_rhobar1 :
	(ms:Ms)
	 (HV_L (rhobar (sc O ms)))=O.

Cut ((m:M)(hv_rhobar_m m))/\((ms:Ms)(hv_rhobar_ms ms)).
(Intros c; Case c; Auto).

Exact HV_rhobar_m.
Save.

Lemma HV_rhobar :
	(m:M)(x:V)(l1,l2:L)
	(rhobar m)=(app x l1 l2)->
	 (HV_L l2)=O.

Cut ((m:M)(hv_rhobar_m m))/\((ms:Ms)(hv_rhobar_ms ms)).
(Intros c; Case c; Auto).

Exact HV_rhobar_m.
Save.
*)

Definition oi_rhobar_m : M->Prop :=
	[m:M](x:V)
	 (Occurs_In_M x m)->
	  (Occurs_In_L x (rhobar m)).

Definition oi_rhobar_ms : Ms->Prop :=
	[ms:Ms](x,y:V)
	 (Occurs_In_Ms x ms)->
	  (Occurs_In_L (S x) (rhobar (sc y (lift_Ms O ms)))).

Lemma oi_rhobar_M :
	((m:M)(oi_rhobar_m m))/\
	 ((ms:Ms)(oi_rhobar_ms ms)).

Apply M_Ms_Height_ind.
(Intro; Case m; Clear  m).
(Intros x ms; Generalize x ; Clear  x; Case ms; Clear  ms).
(Unfold oi_rhobar_ms; Unfold oi_rhobar_m; Intros).
Inversion_clear H0.
Inversion_clear H1.
(Case H; Rewrite -> H0; Clear  H H0 x0; Intros).
(Simpl; Auto).

Inversion H1.

(Unfold oi_rhobar_m; Unfold oi_rhobar_ms; Intros).
(Case H; Clear  H; Inversion_clear H0).
(Inversion_clear H; Rewrite -> H0; Clear  H0 x0; Intros).
Rewrite -> RhoBar2.
Auto.

(Inversion_clear H; Intros).
Rewrite -> RhoBar2.
Apply Occurs_in_app2.
(Apply H; Auto).
(Rewrite -> HTM1; Apply ltS; Rewrite -> HTM4; Apply lt_max_nat1; Auto).

Rewrite -> RhoBar2.
(Apply Occurs_in_app3; Apply H1; Auto).
(Rewrite -> HTM1; Apply ltS; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Apply lt_max_nat1; Auto).

(Unfold oi_rhobar_m; Unfold oi_rhobar_ms; Intros).
(Inversion_clear H0; Rewrite -> RhoBar3; Case H; Clear  H; Intros).
(Apply Occurs_in_lm; Apply H; Auto).
(Rewrite -> HTM2; Apply ltiSi; Auto).

(Intros ms; Case ms; Clear  ms; Unfold oi_rhobar_m; Unfold oi_rhobar_ms;
 Intros).
Inversion H0.

Inversion_clear H0.
(Case H; Clear  H; Intros).
(Rewrite -> LIFTM4; Rewrite -> RhoBar2).
Apply Occurs_in_app2.
(Apply H0; Auto).
Rewrite -> Height_Lift_M.
(Rewrite -> HTM4; Apply lt_max_nat1; Auto).

Apply OIM1_is_OIM2.
Rewrite -> OI_Lift_M1_4.
Unfold pred.
(Apply OIM1_is_OIM1; Auto).

Auto.

(Case H; Clear  H; Intros).
(Rewrite -> LIFTM4; Rewrite -> RhoBar2).
Apply Occurs_in_app3.
(Apply H; Auto).
(Rewrite -> Height_Lift_Ms; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Apply lt_max_nat1; Auto).

(Apply OIMs1_is_OIMs2; Rewrite -> OI_Lift_Ms1_4; Auto;
 Apply OIMs1_is_OIMs1; Unfold pred; Auto).
Save.

Lemma OI_RhoBar_M :
	(m:M)(x:V)
	 (Occurs_In_M x m)->
	  (Occurs_In_L x (rhobar m)).

Cut ((m:M)(oi_rhobar_m m))/\
	 ((ms:Ms)(oi_rhobar_ms ms)).
Intros c; Case c; Unfold oi_rhobar_m; Auto.

Exact oi_rhobar_M.
Save.

Lemma OI_RhoBar_Ms :
	(ms:Ms)(x,y:V)
	 (Occurs_In_Ms x ms)->
	  (Occurs_In_L (S x) (rhobar (sc y (lift_Ms O ms)))).

Cut ((m:M)(oi_rhobar_m m))/\
	 ((ms:Ms)(oi_rhobar_ms ms)).
Intros c; Case c; Unfold oi_rhobar_ms; Auto.

Exact oi_rhobar_M.
Save.

Lemma NOI_RhoBar_M :
	(m:M)(x:V)
	 ~(Occurs_In_L x (rhobar m))->
	  ~(Occurs_In_M x m).

(Unfold not; Intros; Apply H; Apply OI_RhoBar_M; Auto).
Save.

Lemma NOI_RhoBar_Ms :
	(ms:Ms)(x:V)
	 ~(Occurs_In_L (S x) (rhobar (sc O (lift_Ms O ms))))->
	  ~(Occurs_In_Ms x ms).

(Unfold not; Intros; Apply H; Apply OI_RhoBar_Ms; Auto).
Save.

Definition oi_rhobar_m1 : M->Prop :=
	[m:M](x:V)
	 (Occurs_In_L x (rhobar m))->
	  (Occurs_In_M x m).

Definition oi_rhobar_ms1 : Ms->Prop :=
	[ms:Ms](x:V)
	 (Occurs_In_L (S x) (rhobar (sc O (lift_Ms O ms))))->
	  (Occurs_In_Ms x ms).

Lemma oi_rhobar_M1 :
	((m:M)(oi_rhobar_m1 m))/\
	 ((ms:Ms)(oi_rhobar_ms1 ms)).

Apply M_Ms_Height_ind.
(Intro; Case m; Clear  m).
(Intros x ms; Generalize x ; Clear  x; Case ms; Clear  ms).
(Unfold oi_rhobar_m1; Unfold oi_rhobar_ms1; Intros).
(Simpl in H0; Inversion_clear H0; Auto).

(Unfold oi_rhobar_m1; Unfold oi_rhobar_ms1; Intros).
(Case H; Clear  H; Intros).
(Generalize H0 ; Clear  H0; Rewrite -> RhoBar2; Intros).
(Inversion_clear H0; Auto).
(Apply Occurs_in_sc2; Apply Occurs_in_mcons1; Apply H; Auto).
(Rewrite -> HTM1; Apply ltS; Rewrite -> HTM4; Apply lt_max_nat1; Auto).

(Apply Occurs_in_sc2; Apply Occurs_in_mcons2; Apply H1; Auto).
(Rewrite -> HTM1; Apply ltS; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Apply lt_max_nat1; Auto).

(Unfold oi_rhobar_m1; Unfold oi_rhobar_ms1; Intros).
Simpl in H0.
Inversion_clear H0.
(Apply Occurs_in_lambda; Case H; Clear  H; Intros; Apply H; Auto).
(Rewrite -> HTM2; Apply ltiSi; Auto).

(Induction ms; Clear  ms; Unfold oi_rhobar_ms1; Unfold oi_rhobar_m1;
 Intros).
(Simpl in H0; Inversion_clear H0; Inversion_clear H1; Discriminate H0).

(Generalize H1 ; Rewrite -> LIFTM4; Rewrite -> RhoBar2; Case H0;
 Clear  H H0 H1; Intros).
Inversion_clear H1.
(Inversion_clear H2; Discriminate H1).

(Apply Occurs_in_mcons1; Cut x=(pred (S x)); Auto; Intros).
(Rewrite -> H1; Apply OIM1_is_OIM2;
 Rewrite <- (OI_Lift_M1_4 m (S x) O); Auto).
(Apply OIM1_is_OIM1; Apply H0; Auto).
(Rewrite -> Height_Lift_M; Rewrite -> HTM4; Apply lt_max_nat1; Auto).

(Apply Occurs_in_mcons2; Cut x=(pred (S x)); Auto).
(Intros; Rewrite -> H1).
(Apply OIMs1_is_OIMs2; Rewrite <- (OI_Lift_Ms1_4 m0 (S x) O); Auto).
Apply OIMs1_is_OIMs1.
(Apply H; Auto).
(Rewrite -> Height_Lift_Ms; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Apply lt_max_nat1; Auto).
Save.

Lemma OI_RhoBar_M1 :
	(x:V)(m:M)
	 (Occurs_In_L x (rhobar m))->
	  (Occurs_In_M x m).

Cut ((m:M)(oi_rhobar_m1 m))/\
	 ((ms:Ms)(oi_rhobar_ms1 ms)).
Intros c; Case c; Unfold oi_rhobar_m1; Auto.
Exact oi_rhobar_M1.
Save.

Lemma OI_RhoBar_Ms1 :
	(x:V)(ms:Ms)
	 (Occurs_In_L (S x) (rhobar (sc O (lift_Ms O ms))))->
	  (Occurs_In_Ms x ms).

Cut ((m:M)(oi_rhobar_m1 m))/\
	 ((ms:Ms)(oi_rhobar_ms1 ms)).
Intros c; Case c; Unfold oi_rhobar_ms1; Auto.
Exact oi_rhobar_M1.
Save.

Lemma NOI_RhoBar_M1 :
	(x:V)(m:M)
	 ~(Occurs_In_M x m)->
	  ~(Occurs_In_L x (rhobar m)).

(Unfold not; Intros; Apply H; Apply OI_RhoBar_M1; Auto).
Save.

Lemma NOI_RhoBar_Ms1 :
	(x:V)(ms:Ms)
	 ~(Occurs_In_Ms x ms)->
	  ~(Occurs_In_L (S x) (rhobar (sc O (lift_Ms O ms)))).

(Unfold not; Intros; Apply H; Apply OI_RhoBar_Ms1; Auto).
Save.

Lemma Drop_RhoBar_Bridge :
	(x:V)(m:M)
	 ~(Occurs_In_M x m)->
	  (drop_L x (rhobar m))=
	   (rhobar (drop_M x m)).

Intros.
(Rewrite <- (Lift_Drop_M x m); Auto).
Rewrite <- Lift_RhoBar_Bridge.
Rewrite -> Drop_Lift_M.
(Rewrite -> Drop_Lift_L; Auto).
Save.

Lemma Drop_Lift_M_Bridge1 :
	(m:M)(i,j:nat)
         ~(Occurs_In_M i m)->
          (lt j (S i))->
           (drop_M (S i) (lift_M j m))=(lift_M j (drop_M i m)).

Intros.
Rewrite <- (psitheta m).
Rewrite -> Lift_Psi_Bridge.
Rewrite <- Psi_Drop_N_Bridge.
(Rewrite -> Drop_Lift_N_Bridge1; Auto).
Rewrite <- Theta_Drop_M_Bridge.
Rewrite -> Lift_Theta_Bridge.
(Rewrite -> psitheta; Rewrite -> psitheta; Auto).

(Apply NOI_Theta; Auto).
Save.

Lemma Drop_Lift_Ms_Bridge1 :
	(ms:Ms)(i,j:nat)
	 ~(Occurs_In_Ms i ms)->
          (lt j (S i))->
           (drop_Ms (S i) (lift_Ms j ms))=(lift_Ms j (drop_Ms i ms)).

(Induction ms; Clear  ms; Intros).
Auto.

(Rewrite -> LIFTM4; Rewrite -> DROPM4; Rewrite -> Drop_Lift_M_Bridge1;
 Auto).
(Rewrite -> H; Auto).
(Unfold not; Intros; Apply H0; Auto).

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


Definition app_red_m : M->Prop :=
	[m:M](x:V)(m1:M)
	  (L_Permn (app x (rhobar m1) (rhobar m))
		   (rhobar (MsubstVMV x m1 O m))).

Definition app_red_ms : Ms->Prop :=
	[ms:Ms](x,y:V)(m1:M)
	  (L_Permn (app x (rhobar m1) (rhobar (sc y ms)))
		   (app x (rhobar m1) (rhobar (sc y ms)))).

Lemma app_red :
	((m:M)(app_red_m m))/\
	 ((ms:Ms)(app_red_ms ms)).

Apply M_Ms_Height_ind.
(Intro; Case m; Clear  m).
(Intros x ms; Generalize x ; Clear  x; Case ms; Clear  ms).
(Intros x; Case x; Clear  x; Unfold app_red_m; Unfold app_red_ms;
 Intros).
(Apply l_permn_base; Simpl; Auto).

(Simpl; Unfold drop_V; Rewrite -> ltb_is_lt3).
(Simpl; Apply L_Perm1n; Cut (vr n)=(drop_L O (vr (S n))); Auto).
(Intros c; Rewrite -> c; Apply l_perm1_app_wkn; Auto).
(Unfold not; Intros; Inversion_clear H0; Inversion_clear H1;
 Discriminate H0).

(Unfold not; Intros c; Inversion c).

(Unfold app_red_m; Unfold app_red_ms; Intros).
(Case H; Clear  H; Intros).
Clear  H0.
(Generalize H ; Case x; Clear  H x; Intros).
(Rewrite -> MSVMV1; Rewrite -> nateqb_is_eq1; Auto; Unfold Setifb).
(Rewrite -> RhoBar2; Rewrite -> RhoBar2).
(Cut (OIMs_compare O (mcons m m0)); Auto; Unfold OIM_compare; Intros c;
 Case c; Clear  c; Intros).
Apply l_permn_rec with l1:=(app x0 (rhobar m1)
                             (app O
                               (app (lift_V O x0)
                                 (lift_L O (rhobar m1))
                                 (lift_L (S O) (rhobar m)))
                               (app (lifts_V (S (S O)) O x0)
                                 (lifts_L (S (S O)) O (rhobar m1))
                                 (L_Exchange O
                                   (lift_L (S (S O))
                                     (rhobar (sc O (lift_Ms O m0)))))))).
Apply l_perm1_app_app2.
Inversion_clear H0.
(Left; Apply OI_RhoBar_M; Auto).

(Right; Apply OI_RhoBar_Ms; Auto).

Apply Norm'_L_RhoBar.

Apply L_Permn_app2.
(Rewrite -> Lift_RhoBar_Bridge; Rewrite -> Lift_RhoBar_Bridge).
Rewrite -> Lifts_RhoBar_Bridge.
(Rewrite -> MSVMV4; Rewrite -> LIFTM4; Rewrite -> RhoBar2).
Repeat (Rewrite -> Lift_Mssub_Bridge1; Auto).
Cut (MsubstVMV (lift_V O (lift_V O x0)) (lift_M O (lift_M O m1)) O
      (sc (S O) (lift_Ms (S O) (lift_Ms (S O) m0))))
     =(sc O
        (MssubstVMV (lift_V O (lift_V O x0)) (lift_M O (lift_M O m1)) O
          (lift_Ms (S O) (lift_Ms (S O) m0)))).
(Intros; Rewrite <- H1).
Apply L_Permn_app.
(Rewrite -> Lift_Msub_Bridge1; Auto).
(Apply H; Auto).
(Rewrite -> Height_Lift_M; Rewrite -> HTM1; Rewrite -> HTM4; Apply ltS;
 Apply lt_max_nat1; Auto).

(Rewrite -> Lift_RhoBar_Bridge; Rewrite -> Exchange_RhoBar_Bridge).
Clear  H1.
(Rewrite -> LIFTM1; Rewrite -> MExch1).
Unfold 1 lift_V.
(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb; Unfold V_Exchange;
 Rewrite -> nateqb_is_eq1; Auto).
Unfold Setifb.
(Rewrite <- Lift_Lift_Ms_Bridge; Auto).
(Rewrite -> Exchange_Lift_Ms; Auto).
Unfold lifts_V.
(Repeat Rewrite -> Lifts_M_rec1; Rewrite -> Lifts_M0).
(Apply H; Auto).
(Rewrite -> HTM1; Rewrite -> Height_Lift_Ms; Rewrite -> Height_Lift_Ms;
 Rewrite -> HTM1; Apply lt_S; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Apply lt_max_nat1; Auto).

Auto.

(Rewrite -> NOI_Mssub_Bridge; Auto).
(Rewrite -> Lift_Drop_Ms; Auto).
Apply L_Permn_app2.
(Apply L_Permnn with l0:=(rhobar
                           (MsubstVMV O m O (sc O (lift_Ms O m0))));
 Auto).
(Apply H; Auto).
(Rewrite -> HTM1; Rewrite -> HTM1; Apply lt_S;
 Rewrite -> Height_Lift_Ms; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Apply lt_max_nat1; Auto).

(Rewrite -> MSVMV1; Rewrite -> nateqb_is_eq1; Auto; Unfold Setifb).
(Rewrite -> NOI_Mssub_Bridge; Auto).
(Rewrite -> Drop_Lift_Ms; Auto).

Apply NOI_Lift_Ms.

Rewrite -> RhoBar2.
(Rewrite -> MSVMV1; Rewrite -> nateqb_is_eq3; Unfold Setifb).
(Cut (OIMs_compare O (mcons m m0)); Auto; Unfold OIMs_compare;
 Intros c; Case c; Clear  c; Intros).
Unfold drop_V.
(Rewrite -> ltb_is_lt3; Unfold Setifb).
Unfold pred.
Rewrite -> MSVMV4.
Rewrite -> RhoBar2.
Apply l_permn_rec with l1:=(app n (app x0 (rhobar m1) (rhobar m))
                             (app (lift_V O x0) (lift_L O (rhobar m1))
                               (L_Exchange O
                                 (rhobar (sc O (lift_Ms O m0)))))).
(Apply l_perm1_app_app1; Auto).
Inversion_clear H0.
(Left; Apply OI_RhoBar_M; Auto).

(Right; Apply OI_RhoBar_Ms; Auto).

Apply Norm'_L_RhoBar.

Apply L_Permn_app.
(Apply H; Auto).
(Rewrite -> HTM1; Apply ltS; Rewrite -> HTM4; Apply lt_max_nat1; Auto).

Rewrite -> Exchange_RhoBar_Bridge.
Rewrite -> MExch1.
(Unfold V_Exchange; Rewrite -> nateqb_is_eq1; Auto; Unfold Setifb).
Rewrite -> Exchange_Lift_Ms.
Rewrite -> Lift_RhoBar_Bridge.
(Apply L_Permnn with l0:=(rhobar
                           (MsubstVMV (lift_V O x0) (lift_M O m1) O
                             (sc (S O) (lift_Ms (S O) m0)))); Auto).
(Apply H; Auto).
(Rewrite -> HTM1; Rewrite -> HTM1; Apply lt_S;
 Rewrite -> Height_Lift_Ms; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Apply lt_max_nat1; Auto).

(Rewrite -> MSVMV1; Rewrite -> nateqb_is_eq3; Unfold Setifb).
Unfold drop_V.
Unfold ltb.
Unfold Setifb.
Unfold pred.
(Rewrite -> Lift_Mssub_Bridge1; Auto).

Discriminate.

Auto.

(Unfold not; Intros x; Inversion x).

Unfold drop_V.
(Unfold ltb; Unfold Setifb).
Unfold pred.
(Rewrite -> MSVMV4; Rewrite -> RhoBar2).
Rewrite -> NOI_Mssub_Bridge.
Rewrite -> NOI_Msub_Bridge.
Apply l_permn_rec with l1:=(drop_L O
                             (app (S n) (rhobar m)
                               (rhobar (sc O (lift_Ms O m0))))).
(Apply l_perm1_app_wkn; Auto).
(Apply OIL1_is_OIL4; Rewrite -> Occurs_In_L1_eq2; Apply ororb1; 
 Split; Auto; Apply ororb1; Split; Apply OIL1_is_OIL3).
Apply NOI_RhoBar_M1.
(Unfold not; Intros; Apply H0; Auto).

Apply NOI_RhoBar_Ms1.
(Unfold not; Intros; Apply H0; Auto).

Rewrite -> drop_L_eq2.
Unfold drop_V.
Unfold ltb.
Unfold Setifb.
Rewrite -> Drop_RhoBar_Bridge.
Rewrite -> Drop_RhoBar_Bridge.
Rewrite -> DROPM1.
(Unfold drop_V; Unfold ltb; Unfold Setifb).
(Rewrite -> Drop_Lift_Ms_Bridge1; Auto).
(Unfold not; Intros; Auto_Contra H0).

(Apply OIM1_is_OIM4; Rewrite -> OIM1; Apply ororb1; Split; Auto).
(Rewrite -> OI_Lift_Ms1_4; Auto).
(Unfold pred; Apply OIMs1_is_OIMs3; Unfold not; Intros; Auto_Contra H0).

(Unfold not; Intros; Auto_Contra H0).

(Unfold not; Intros; Auto_Contra H0).

(Unfold not; Intros; Auto_Contra H0).

Discriminate.

(Unfold app_red_m; Unfold app_red_ms; Intros).
Simpl.
(Case H; Clear  H; Intros).
Clear  H0.
Apply l_permn_rec with l1:=(lm
                             (app (lift_V O x) (lift_L O (rhobar m1))
                               (L_Exchange O (rhobar m)))).
Apply l_perm1_app_lm.

Rewrite -> Exchange_RhoBar_Bridge.
Apply L_Permn_lm.
Rewrite -> Lift_RhoBar_Bridge.
Apply L_Permnn with l0:=(rhobar
                          (MsubstVMV (lift_V O x) (lift_M O m1) O
                            (M_Exchange O m))).
(Apply H; Auto).
Rewrite -> Height_M_Exchange.
(Rewrite -> HTM2; Apply ltiSi; Auto).

(Rewrite -> Msub_Exch_Bridge1; Auto).

(Unfold app_red_ms; Auto).
Save.

Lemma App_Red_M :
	(x:V)(m1,m:M)
	 (L_Permn (app x (rhobar m1) (rhobar m))
		  (rhobar (MsubstVMV x m1 O m))).

Cut ((m:M)(app_red_m m))/\
	 ((ms:Ms)(app_red_ms ms)).
Intros c; Case c; Unfold app_red_m; Auto.
Exact app_red.
Save.

Lemma Norm_Red :
	(l:L)(L_Permn l (rhobar (phibar l))).

(Induction l; Clear  l; Auto; Intros).
Simpl.
Apply L_Permnn with l0:=(app v (rhobar (phibar l)) (rhobar (phibar l0))).
(Apply L_Permn_app; Auto).

Apply App_Red_M.

(Simpl; Apply L_Permn_lm; Auto).
Save.