Require MinMJ_Lifts.
Require MinMJ_HeightM.

(* The Mapping RhoBar from MJ to LJ. *)
Fixpoint
    rhobar [m:M] : L :=
	<L>Case m of
	    (* x;ms *)[x:V][ms:Ms]
		<L>Case ms of
		    (* mnil *)
			(vr x)
		    (* m::ms *)[m:M][ms:Ms]
			(app x (rhobar m) (rhobar' ms (S O)))
		end
	    (* \m *)[m:M]
		(lm (rhobar m))
	end
with
    rhobar' [ms:Ms] : nat->L :=
	[i:nat]
	<L>Case ms of
	    (* mnil *)
		(vr O)
	    (* m::ms *)[m:M][ms:Ms]
		(app O (lifts_L i O (rhobar m)) (rhobar' ms (S i)))
	end.

Recursive Definition rhobar1 : nat->Ms->L :=
i ms => (rhobar' ms i).

Recursive Definition rho : N->L :=
n => (rhobar (psi n)).

Lemma rhothetarhobar : (m:M)
	(rho (theta m))=(rhobar m).

Lemma Rhobar1 : (x:V)
	(rhobar (sc x mnil))=(vr x).

Lemma Rhobar2 : (x:V)(m:M)
	(rhobar (sc x (mcons m mnil)))=
	 (app x (rhobar m) (vr O)).

Lemma Rhobar3 : (x:V)(m:M)(ms:Ms)
	(rhobar (sc x (mcons m ms)))=
	 (app x (rhobar m) (rhobar1 (S O) ms)).

Lemma Rhobar4 : (m:M)
	(rhobar (lambda m))=(lm (rhobar m)).

Lemma Rhobar5 : (i:nat)
	(rhobar1 i mnil)=(vr O).

Lemma Rhobar6 : (m:M)(ms:Ms)(i:nat)
	(rhobar1 i (mcons m ms))=
	 (app O
	      (lifts_L i O (rhobar m))
	      (rhobar1 (S i) ms)).

Definition phibarrhobar1 : M->Prop :=
	[m:M]
	 (phibar (rhobar m))=m.

Definition phibarrhobar2 : Ms->Prop :=
	[ms:Ms]
	 (m:M)(i:nat)
	  ((m1:M)
	    (lt (Height_M m1) (Height_Ms (mcons m ms)))->
	     (phibar (rhobar m1))=m1)->
	   (phibar (rhobar1 i (mcons m ms)))=
	    (sc O (lifts_Ms i O (mcons m ms))).

Lemma Phibarrhobar :
	((m:M)(phibarrhobar1 m))/\
	 ((ms:Ms)(phibarrhobar2 ms)).

Lemma phibarrhobar :
	(m:M)(phibar (rhobar m))=m.

Lemma phibarrhobar_ms :
	(i:nat)(m:M)(ms:Ms)
	 (phibar (rhobar1 i (mcons m ms)))=
	    (sc O (lifts_Ms i O (mcons m ms))).

Lemma phirho : (n:N)(phi (rho n))=n.