Require Export MinMJ_NormL.
Require Export MinMJ_PermDef.
Require Export MinMJ_HeightL.

Lemma perm_not_norm_l1 :
	(l0,l1,l2:L)(x:V)
	 (Occurs_In_L O l1)->
	  ~(Norm_L (app x l0 (app O l1 l2))).

Lemma perm_not_norm_l2 :
	(l0,l1,l2:L)(x:V)
	 (Occurs_In_L (S O) l2)->
	  ~(Norm_L (app x l0 (app O l1 l2))).

Lemma Norm'_Norm_L :
	(l:L)
	 (Norm'_L l)->
	  (Norm_L l).

Lemma Perm_not_norm_l : 
	(l0,l1:L)
	 (L_Perm1 l0 l1)->
	  ~(Norm_L l0).

Lemma Perm_Not_Norm_L :
	(l0,l1:L)
	 (L_Perm1 l0 l1)->
	  ~(Norm_L l0).

Lemma Norm_Imperm_L :
	(l0,l1:L)
	 (Norm_L l0)->
	  ~(L_Perm1 l0 l1).