(*#* #stop file *)

Require tlt_defs.
Require lift_tlt.
Require subst0_defs.

   Section subst0_tlt_props. (***********************************************)

      Theorem subst0_weight_le : (u,t,z:?; d:?) (subst0 d u t z) ->
                                 (f,g:?) ((m:?) (le (f m) (g m))) ->
                                 (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
                                 (le (weight_map f z) (weight_map g t)).
      Intros until 1; XElim H.
(* case 1: subst0_lref *)
      Intros; XAuto.
(* case 2: subst0_fst *)
      XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
(* case 3: subst0_snd *)
      XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
(* case 4: subst0_both *)
      XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
      Qed.

      Theorem subst0_weight_lt : (u,t,z:?; d:?) (subst0 d u t z) -> (f,g:?)
                                 ((m:?) (le (f m) (g m))) ->
                                 (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
                                 (lt (weight_map f z) (weight_map g t)).
      Intros until 1; XElim H.
(* case 1: subst0_lref *)
      Intros; XAuto.
(* case 2: subst0_fst *)
      XElim k; [ XElim b | Idtac ]; Simpl; Intros;
      Apply lt_n_S; (Apply lt_le_plus_plus; [ XAuto | Idtac ]); (**)
      [ Auto 6 with ltlc (**) | XAuto | XAuto | XAuto ].
(* case 3: subst0_snd *)
      XElim k; [ XElim b | Idtac ]; Simpl;
      [ Auto 8 with ltlc | Auto 6 with ltlc | Auto 6 with ltlc | XAuto ]. (**)
(* case 3: subst0_both *)
      XElim k; [ XElim b | Idtac ]; Simpl;
      Intros; Apply lt_n_S; [ Apply lt_le_plus_plus | Apply lt_plus_plus | Apply lt_plus_plus | Apply lt_plus_plus ]; XAuto.
      EApply subst0_weight_le; [ XEAuto | XAuto | XAuto ].
      Qed.

      Theorem subst0_tlt_tail: (u,t,z:?) (subst0 (0) u t z) ->
                               (tlt (TTail (Bind Abbr) u z)
                                    (TTail (Bind Abbr) u t)
                               ).
      Unfold tlt weight; Intros; Simpl.
      Apply lt_n_S; Apply le_lt_plus_plus; [ XAuto | Idtac ].
      EApply subst0_weight_lt; [ XEAuto | XAuto | XAuto ].
      Qed.

      Theorem subst0_tlt: (u,t,z:?) (subst0 (0) u t z) ->
                          (tlt z (TTail (Bind Abbr) u t)).
      Intros.
      EApply tlt_trans; [ Idtac | Apply subst0_tlt_tail; XEAuto].
      XAuto.
      Qed.

   End subst0_tlt_props.

      Hints Resolve subst0_tlt : ltlc.