Require MinMJ_Lift.

Fixpoint
    Height_M [m:M] : nat :=
	<nat>Case m of
	(* sc x ms *)[x:V][ms:Ms](S (Height_Ms ms))
	(* lambda m *)[m:M](S (Height_M m))
	end with
    Height_Ms [ms:Ms] : nat :=
	<nat>Case ms of
	(* mnil *)O
	(* mcons m ms *)[m:M][ms:Ms](S (max_nat (Height_M m) (Height_Ms ms)))
	end.

Lemma HTM1 : (x:V)(ms:Ms)
	(Height_M (sc x ms))=(S (Height_Ms ms)).

Lemma HTM2 : (m:M)
	(Height_M (lambda m))=(S (Height_M m)).

Lemma HTM3 :
	(Height_Ms mnil)=O.

Lemma HTM4 : (m:M)(ms:Ms)
	(Height_Ms (mcons m ms))=(S (max_nat (Height_M m) (Height_Ms ms))).

Lemma Height_Ms_Zero_Nil1 : (ms:Ms)
	~ms=mnil->
	 (lt O (Height_Ms ms)).

Lemma Height_Ms_Zero_Nil : (ms:Ms)
	(Height_Ms ms)=O->
	 ms=mnil.

Lemma Height_M_not_eq_not_eq :
	(m:M)(m0:M)
	 ~(Height_M m)=(Height_M m0)->
	  ~m=m0.

Lemma Height_Ms_not_eq_not_eq :
	(ms:Ms)(ms0:Ms)
	 ~(Height_Ms ms)=(Height_Ms ms0)->
	  ~ms=ms0.

Definition height_lift_m : M->Prop :=
	[m:M](i:nat)
	 (Height_M (lift_M i m))=
	  (Height_M m).

Definition height_lift_ms : Ms->Prop :=
	[ms:Ms](i:nat)
	 (Height_Ms (lift_Ms i ms))=
	  (Height_Ms ms).

Lemma height_lift_M :
	((m:M)(height_lift_m m))/\
	 ((ms:Ms)(height_lift_ms ms)).

Lemma Height_Lift_M :
	(m:M)(i:nat)
	 (Height_M (lift_M i m))=
	  (Height_M m).

Lemma Height_Lift_Ms :
	(ms:Ms)(i:nat)
	 (Height_Ms (lift_Ms i ms))=
	  (Height_Ms ms).

Section HeightMind.

Variable P:M->Prop.
Variable P0:Ms->Prop.

Definition QSM : M->Prop :=
	[m:M]
	 ((m1:M)
	   ((lt (Height_M m1) (Height_M m)) \/
	     (Height_M m1)=(Height_M m))->
	    (P m1))/\
	 ((ms1:Ms)
	   ((lt (Height_Ms ms1) (Height_M m)) \/
	     (Height_Ms ms1)=(Height_M m))->
	    (P0 ms1)).

Definition QSMs : Ms->Prop :=
	[ms:Ms]
	 ((m1:M)
	   ((lt (Height_M m1) (Height_Ms ms)) \/
	     (Height_M m1)=(Height_Ms ms))->
	    (P m1))/\
	 ((ms1:Ms)
	   ((lt (Height_Ms ms1) (Height_Ms ms)) \/
	     (Height_Ms ms1)=(Height_Ms ms))->
	    (P0 ms1)).

Lemma M_Ms_szind1 :
	(((m:M)(QSM m))/\((ms:Ms)(QSMs ms)))->
	 ((m:M)(P m))/\((ms:Ms)(P0 ms)).

Lemma M_Ms_Height_ind :
   ((m:M)
     (((m1:M)(lt (Height_M m1) (Height_M m))->(P m1)) /\
     ((ms1:Ms)(lt (Height_Ms ms1) (Height_M m))->(P0 ms1)))->(P m))->
     ((ms:Ms)
        (((ms1:Ms)(lt (Height_Ms ms1) (Height_Ms ms))->(P0 ms1))/\
        ((m1:M)(lt (Height_M m1) (Height_Ms ms))->(P m1)))->(P0 ms))->
         ((m:M)(P m))/\((ms:Ms)(P0 ms)).

End HeightMind.