Require MinMJ_Nsub.

(* The Mapping Phi from LJ to NJ. *)
Recursive Definition
    phi : L -> N :=
	(vr x) => (an (var x)) |
	(app x l1 l2) =>
		(NsubstAV (ap (var x) (phi l1)) O (phi l2)) |
	(lm l) => (lam (phi l)).