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).

Unfold well_founded .
(Induction a; Clear  a; Intros).
Apply Acc_intro.
Unfold lt_Height_L .
Simpl.
Intros.
Inversion H.

Apply Acc_intro.
Unfold lt_Height_L .
Rewrite -> Height_L_eq2.
Intros.
Cut (or
      (and (lt (Height_L y) (S (Height_L l)))
        (lt (Height_L l0) (S (Height_L l))))
      (and (lt (Height_L y) (S (Height_L l0)))
        (lt (Height_L l) (S (Height_L l0))))).
(Intros c; Case c; Clear  c H1; Intros c; Case c; Clear  c; Intros).
Cut (or (lt (Height_L y) (Height_L l)) (eq ? (Height_L y) (Height_L l))).
(Intros c; Case c; Clear  c H1; Intros).
Apply Acc_inv with x:=l.
Unfold lt_Height_L  in H.
Auto.

Auto.

Apply Acc_intro.
Intros.
(Generalize H3 ; Clear  H3; Rewrite -> H1; Intros).
(Apply Acc_inv with x:=l; Auto).

(Apply lt_S_le2; Auto).

Cut (or (lt (Height_L y) (Height_L l0)) (eq ? (Height_L y) (Height_L l0))).
(Intros c; Case c; Clear  c H1; Intros).
(Apply Acc_inv with x:=l0; Auto).

(Apply Acc_intro; Rewrite -> H1; Intros).
(Apply Acc_inv with x:=l0; Auto).

(Apply lt_S_le2; Auto).

(Apply lt_max_nat; Auto).

(Apply Acc_intro; Unfold 1 lt_Height_L ; Simpl; Intros).
Cut (or (lt (Height_L y) (Height_L l)) (eq ? (Height_L y) (Height_L l))).
(Intros c; Case c; Clear  c H0; Intros).
(Apply Acc_inv with x:=l; Auto).

(Apply Acc_intro; Unfold lt_Height_L ; Rewrite -> H0; Intros).
(Apply Acc_inv with x:=l; Auto).

(Apply lt_S_le2; Auto).
Save.

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

(Intros; Apply (well_founded_ind L lt_Height_L WF_Height_L); Auto).
Save.

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).

(Intros; Apply L_Height_ind1; Auto).
Save.

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

(Induction l; Clear  l; Intros; Auto; Simpl).
(Rewrite -> H; Rewrite -> H0; Auto).

(Rewrite -> H; Auto).
Save.