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

Auto.
Save.

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

Auto.
Save.

Lemma HTM3 :
	(Height_Ms mnil)=O.

Auto.
Save.

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

Auto.
Save.

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

(Induction ms; Auto; Clear  ms).
(Intros; Cut False; Auto; Contradiction).

Intros.
Rewrite -> HTM4.
Auto.
Save.

Lemma Height_Ms_Zero_Nil : (ms:Ms)
	(Height_Ms ms)=O->
	 ms=mnil.
(Induction ms; Clear  ms; Auto; Intros m ms).
Rewrite -> HTM4.
Intros.
Discriminate H0.
Save.

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

Unfold not; Intros; Apply H; Rewrite <- H0; Auto.
Save.

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

Unfold not; Intros; Apply H; Rewrite <- H0; Auto.
Save.

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

(Apply M_Ms_ind; Unfold height_lift_m ; Unfold height_lift_ms ; Intros; Auto).
(Rewrite -> LIFTM1; Rewrite -> HTM1; Rewrite -> H; Auto).

(Rewrite -> LIFTM2; Rewrite -> HTM2; Rewrite -> H; Auto).

(Rewrite -> LIFTM4; Rewrite -> HTM4; Rewrite -> H; Rewrite -> H0; Auto).
Save.

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

Cut ((m:M)(height_lift_m m))/\
	 ((ms:Ms)(height_lift_ms ms)).
Intros c; Case c; Auto.
Exact height_lift_M.
Save.

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

Cut ((m:M)(height_lift_m m))/\
	 ((ms:Ms)(height_lift_ms ms)).
Intros c; Case c; Auto.
Exact height_lift_M.
Save.

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

(Intros H; Case H; Clear  H; Unfold QSM ; Unfold QSMs ; Intros;
 Apply M_Ms_ind; Intros).
Case (H0 (mcons (sc v m) mnil)).
(Intros; Apply H2; Rewrite -> HTM1; Rewrite -> HTM4).
Rewrite -> HTM3.
Rewrite -> max_nat0.
(Rewrite -> HTM1; Left; Apply ltiSi; Auto).

(Case (H (lambda (lambda m))); Intros).
Apply H2.
Left.
Simpl.
(Apply ltiSi; Auto).

(Case (H0 mnil); Auto).

(Case (H0 (mcons m m0)); Auto).
Save.

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

(Intros; Apply M_Ms_szind1).
(Apply M_Ms_ind; Unfold QSM; Unfold QSMs; Intros; Auto).
(Split; Intros).
(Case H1; Clear  H1; Intros; Case H2; Clear  H2; Intros).
(Generalize H2 ; Clear  H2; Rewrite -> HTM1; Intros).
Cut (S (Height_M m1))=(S (Height_Ms m))
    \/(lt (S (Height_M m1)) (S (Height_Ms m))).
(Intros c; Case c; Clear  c H2; Intros).
(Injection H2; Clear  H2; Intros).
(Apply H1; Auto).

(Inversion_clear H2; Apply H1; Auto).

(Apply lt_S_le; Auto).

(Generalize H2 ; Clear  H2; Rewrite -> HTM1; Intros).
(Apply H; Split; Intros).
(Generalize H4 ; Clear  H4; Rewrite -> H2; Intros).
Cut (S (Height_M m0))=(S (Height_Ms m))
    \/(lt (S (Height_M m0)) (S (Height_Ms m))).
(Intros c; Case c; Clear  c H4; Intros).
(Injection H4; Clear  H4; Intros).
(Apply H1; Auto).

(Inversion_clear H4; Apply H1; Auto).

(Apply lt_S_le; Auto).

(Generalize H4 ; Clear  H4; Rewrite -> H2; Intros).
Cut (S (Height_Ms ms1))=(S (Height_Ms m))
    \/(lt (S (Height_Ms ms1)) (S (Height_Ms m))).
(Intros c; Case c; Clear  c H4; Intros).
(Injection H4; Clear  H4; Intros).
(Apply H3; Auto).

(Inversion_clear H4; Apply H3; Auto).

(Apply lt_S_le; Auto).

(Case H1; Clear  H1; Intros; Case H2; Clear  H2; Rewrite -> HTM1;
 Intros).
Cut (S (Height_Ms ms1))=(S (Height_Ms m))
    \/(lt (S (Height_Ms ms1)) (S (Height_Ms m))).
(Intros c; Case c; Clear  c H2; Intros; Apply H3).
(Injection H2; Auto).

(Inversion_clear H2; Auto).

(Apply lt_S_le; Auto).

(Apply H0; Split; Rewrite -> H2; Intros).
Cut (S (Height_Ms ms0))=(S (Height_Ms m))
    \/(lt (S (Height_Ms ms0)) (S (Height_Ms m))).
(Intros c; Case c; Clear  c H4; Intros; Apply H3).
(Injection H4; Auto).

(Inversion_clear H4; Auto).

(Apply lt_S_le; Auto).

Cut (S (Height_M m1))=(S (Height_Ms m))
    \/(lt (S (Height_M m1)) (S (Height_Ms m))).
(Intros c; Case c; Clear  c H4; Intros; Apply H1).
(Injection H4; Auto).

(Inversion_clear H4; Auto).

(Apply lt_S_le; Auto).

(Split; Intros).
(Case H1; Clear  H1; Intros; Case H2; Clear  H2; Intros).
(Generalize H2 ; Clear  H2; Rewrite -> HTM2; Intros).
Cut (S (Height_M m1))=(S (Height_M m))\/(lt (S (Height_M m1)) (S (Height_M m))).
(Intros c; Case c; Clear  c H2; Intros).
(Injection H2; Clear  H2; Intros).
(Apply H1; Auto).

(Inversion_clear H2; Apply H1; Auto).

(Apply lt_S_le; Auto).

(Generalize H2 ; Clear  H2; Rewrite -> HTM2; Intros).
(Apply H; Split; Intros).
(Generalize H4 ; Clear  H4; Rewrite -> H2; Intros).
Cut (S (Height_M m0))=(S (Height_M m))\/(lt (S (Height_M m0)) (S (Height_M m))).
(Intros c; Case c; Clear  c H4; Intros).
(Injection H4; Clear  H4; Intros).
(Apply H1; Auto).

(Inversion_clear H4; Apply H1; Auto).

(Apply lt_S_le; Auto).

(Generalize H4 ; Clear  H4; Rewrite -> H2; Intros).
Cut (S (Height_Ms ms1))=(S (Height_M m))
    \/(lt (S (Height_Ms ms1)) (S (Height_M m))).
(Intros c; Case c; Clear  c H4; Intros).
(Injection H4; Clear  H4; Intros).
(Apply H3; Auto).

(Inversion_clear H4; Apply H3; Auto).

(Apply lt_S_le; Auto).

(Case H1; Clear  H1; Intros; Case H2; Clear  H2; Rewrite -> HTM2;
 Intros).
Cut (S (Height_Ms ms1))=(S (Height_M m))
    \/(lt (S (Height_Ms ms1)) (S (Height_M m))).
(Intros c; Case c; Clear  c H2; Intros; Apply H3).
(Injection H2; Auto).

(Inversion_clear H2; Auto).

(Apply lt_S_le; Auto).

(Apply H0; Split; Rewrite -> H2; Intros).
Cut (S (Height_Ms ms0))=(S (Height_M m))
    \/(lt (S (Height_Ms ms0)) (S (Height_M m))).
(Intros c; Case c; Clear  c H4; Intros; Apply H3).
(Injection H4; Auto).

(Inversion_clear H4; Auto).

(Apply lt_S_le; Auto).

Cut (S (Height_M m1))=(S (Height_M m))\/(lt (S (Height_M m1)) (S (Height_M m))).
(Intros c; Case c; Clear  c H4; Intros; Apply H1).
(Injection H4; Auto).

(Inversion_clear H4; Auto).

(Apply lt_S_le; Auto).

(Split; Rewrite -> HTM3; Intros; Case H1; Clear  H1; Intros).
Inversion H1.

(Generalize H1 ; Elim m1; Clear  H1 m1).
(Intros x ms; Rewrite -> HTM1).
Intros.
(Rewrite -> (Height_Ms_Zero_Nil ms); Auto).
Discriminate H1.

Discriminate H1.

(Intros m; Rewrite -> HTM2).
Intros.
Discriminate H2.

Inversion H1.

(Rewrite -> (Height_Ms_Zero_Nil ms1); Auto).
(Apply H0; Rewrite -> HTM3; Split; Intros; Inversion H2).

(Rewrite -> HTM4; Case H1; Clear  H1; Intros; Case H2; Clear  H2;
 Intros; Split; Intros; Case H5; Clear  H5; Intros).
Cut (lt (Height_M m1) (S (Height_M m)))/\(lt (Height_Ms m0) (S (Height_M m)))
    \/(lt (Height_M m1) (S (Height_Ms m0)))
      /\(lt (Height_M m) (S (Height_Ms m0))).
(Intros c; Case c; Clear  c H5; Intros c; Case c; Clear  c; Intros).
(Apply H1; Apply lt_S_le2; Auto).

(Apply H2; Apply lt_S_le2; Auto).

(Apply lt_max_nat; Auto).

Cut (Height_M m1)=(S (Height_M m))/\(lt (Height_Ms m0) (S (Height_M m)))
    \/(Height_M m1)=(S (Height_Ms m0))/\(lt (Height_M m) (S (Height_Ms m0))).
(Intros c; Case c; Clear  c H5; Intros c; Case c; Clear  c; Intros).
(Apply H; Split; Intros).
Apply H1.
Apply lt_S_le2.
(Rewrite <- H5; Auto).

(Apply H3; Apply lt_S_le2).
(Rewrite <- H5; Auto).

(Apply H; Split; Intros).
(Apply H2; Apply lt_S_le2; Rewrite <- H5; Auto).

(Apply H4; Apply lt_S_le2; Rewrite <- H5; Auto).

(Apply eq_max_nat; Auto).

Cut (lt (Height_Ms ms1) (S (Height_M m)))/\(lt (Height_Ms m0) (S (Height_M m)))
    \/(lt (Height_Ms ms1) (S (Height_Ms m0)))
      /\(lt (Height_M m) (S (Height_Ms m0))).
(Intros c; Case c; Clear  c H5; Intros c; Case c; Clear  c; Intros).
(Apply H3; Apply lt_S_le2; Auto).

(Apply H4; Apply lt_S_le2; Auto).

(Apply lt_max_nat; Auto).

Cut (Height_Ms ms1)=(S (Height_M m))/\(lt (Height_Ms m0) (S (Height_M m)))
    \/(Height_Ms ms1)=(S (Height_Ms m0))/\(lt (Height_M m) (S (Height_Ms m0))).
(Intros c; Case c; Clear  c H5; Intros c; Case c; Clear  c; Intros).
(Apply H0; Split; Intros).
(Apply H3; Apply lt_S_le2; Rewrite <- H5; Auto).

(Apply H1; Apply lt_S_le2; Rewrite <- H5; Auto).

(Apply H0; Split; Intros).
(Apply H4; Apply lt_S_le2; Rewrite <- H5; Auto).

(Apply H2; Apply lt_S_le2; Rewrite <- H5; Auto).

(Apply eq_max_nat; Auto).
Save.

End HeightMind.