Require MinMJ_Msub.

(* The Mapping PhiBar from LJ to MJ. *)
Recursive Definition
    phibar : L->M :=
	(vr x) => (sc x mnil) |
	(app x l1 l2) => 
		(MsubstVMV x (phibar l1) O (phibar l2)) |
	(lm l) => (lambda (phibar l)).