Require Export MinMJ_Lifts.
Require Export MinMJ_LJ.
Require Export MinMJ_Exchange3.
Require Export MinMJ_NormL.

Inductive 
    L_Perm1 : L->L->Prop :=
	l_perm1_lm : 
		(l1,l2:L)
		   (L_Perm1 l1 l2)->
		    (L_Perm1 (lm l1) (lm l2)) |
 	l_perm1_app1 :
		(i:V)(l11,l12,l2:L)
		   (L_Perm1 l11 l12)->
		     (L_Perm1 (app i l11 l2) (app i l12 l2)) |
 	l_perm1_app2 :
		(i:V)(l1,l21,l22:L)
		    (L_Perm1 l21 l22)->
		      (L_Perm1 (app i l1 l21) (app i l1 l22)) |
 	l_perm1_app_wkn :
		(x:V)(l1,l2:L)
		 ~(Occurs_In_L O l2)->
		  (L_Perm1 (app x l1 l2) (drop_L O l2)) |
	l_perm1_app_app1 :
		(x,z:V)(l1,l2,l3:L)
		 ((Occurs_In_L O l2)\/(Occurs_In_L (S O) l3))->
		  (Norm'_L l3)->
		   (L_Perm1 (app x l1 (app (S z) l2 l3))
			    (app z
				 (app x l1 l2)
				 (app (lift_V O x)
				      (lift_L O l1)
				      (L_Exchange O l3)))) |
 	l_perm1_app_app2 :
		(x:V)(l1,l2,l3:L)
		 ((Occurs_In_L O l2)\/(Occurs_In_L (S O) l3))->
		  (Norm'_L l3)->
		   (L_Perm1 (app x l1 (app O l2 l3))
			    (app x 
				 l1
				 (app O
				      (app (lift_V O x)
					   (lift_L O l1)
					   (lift_L (S O) l2))
				      (app (lifts_V (S (S O)) O x)
					   (lifts_L (S (S O)) O l1)
					   (L_Exchange O 
					     (lift_L (S (S O)) l3)))))) |
	l_perm1_app_lm : (x:V)(l1,l2:L)
		    (L_Perm1 (app x l1 (lm l2))
			     (lm (app (lift_V O x)
				      (lift_L O l1)
				      (L_Exchange O l2)))).

Scheme L_Perm1_ind1 := Induction for L_Perm1 Sort Prop.