(*#* #stop file *)

Require lift_defs.

   Section lift_props. (*****************************************************)

      Theorem lift_free: (t:?; h,k,d,e:?) (le e (plus d h)) -> (le d e) ->
                         (lift k e (lift h d t)) = (lift (plus k h) d t).
      XElim t; Intros.
(* case 1: TSort *)
      Repeat Rewrite lift_sort; XAuto.
(* case 2: TBRef n *)
      Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
      Repeat Rewrite lift_bref_lt; XEAuto.
(* case 2.2: n >= d *)
      Repeat Rewrite lift_bref_ge; XEAuto.
(* case 3: TTail k *)
      LiftTailRw; XAuto.
      Qed.

      Theorem lift_d : (t:?; h,k,d,e:?) (le e d) ->
                       (lift h (plus k d) (lift k e t)) = (lift k e (lift h d t)).
      XElim t; Intros.
(* case 1: TSort *)
      Repeat Rewrite lift_sort; XAuto.
(* case 2: TBRef n *)
      Apply (lt_le_e n e); Intros.
(* case 2.1: n < e *)
      Cut (lt n d); Intros; Repeat Rewrite lift_bref_lt; XEAuto.
(* case 2.2: n >= e *)
      Rewrite lift_bref_ge; [ Idtac | XAuto ].
      Rewrite plus_sym; Apply (lt_le_e n d); Intros.
(* case 2.2.1: n < d *)
      Do 2 (Rewrite lift_bref_lt; [ Idtac | XAuto ]).
      Rewrite lift_bref_ge; XAuto.
(* case 2.2.2: n >= d *)
      Repeat Rewrite lift_bref_ge; XAuto.
(* case 3: TTail k *)
      LiftTailRw; SRw; XAuto.
      Qed.

   End lift_props.