Require MinMJ_In.

Inductive
    L:Set :=
	vr : V->L |
	app : V->L->L->L |
	lm : L->L.