Require MinMJ_Lift.

Recursive Definition
    Height_L : L->nat :=
	(vr x) => O |
	(app x l1 l2) => (S (max_nat (Height_L l1) (Height_L l2))) |
	(lm l) => (S (Height_L l)).

Definition
    lt_Height_L : L->L->Prop :=
	[l1,l2:L](lt (Height_L l1) (Height_L l2)).

Lemma WF_Height_L :
	(well_founded L lt_Height_L).

Lemma L_Height_ind1 :
	(P:L->Prop)
	 ((l0:L)((l1:L)(lt_Height_L l1 l0)->(P l1))->(P l0))->
	  (l:L)(P l).

Lemma L_Height_ind :
	(P:L->Prop)
	 ((l0:L)((l1:L)(lt (Height_L l1) (Height_L l0))->(P l1))->(P l0))->
	  (l:L)(P l).

Lemma Height_Lift_L :
	(l:L)(i:nat)
	 (Height_L (lift_L i l))=
	  (Height_L l).