Require MinMJ_L_Admis_RhoBar.
Require MinMJ_NormL.

Definition noi_rhobar1 : M->Prop :=
	[m:M](i:nat)
	 ~(Occurs_In_L (S i)
	  (rhobar (lift_M i (lift_M i m)))).

Definition noi_rhobar2 : Ms->Prop :=
	[ms:Ms](i:nat)
	 ~(Occurs_In_L (S i)
	  (rhobar (sc O (lift_Ms i (lift_Ms i ms))))).

Lemma noi_rhobar :
	((m:M)(noi_rhobar1 m))/\
	 ((ms:Ms)(noi_rhobar2 ms)).

Lemma NOI_RhoBar1 :
	(m:M)(i:nat)
	 ~(Occurs_In_L (S i)
	  (rhobar (lift_M i (lift_M i m)))).

Lemma NOI_RhoBar2 :
	(ms:Ms)(i:nat)
	 ~(Occurs_In_L (S i)
	  (rhobar (sc O (lift_Ms i (lift_Ms i ms))))).

Definition norm_l_rhobar_m : M->Prop :=
	[m:M](Norm_L (rhobar m)).

Definition norm_l_rhobar_ms : Ms->Prop :=
	[ms:Ms]
	  (Norm'_L (rhobar (sc O (lift_Ms O ms)))).

Lemma norm_l_rhobar :
	((m:M)(norm_l_rhobar_m m))/\
	 ((ms:Ms)(norm_l_rhobar_ms ms)).

Lemma Norm_L_RhoBar : (m:M)
	(Norm_L (rhobar m)).

Lemma Norm'_L_RhoBar : (ms:Ms)
	(Norm'_L (rhobar (sc O (lift_Ms O ms)))).