(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require lift_props.
Require drop1_defs.

   Section ptrans_props. (***************************************************)

      Hints Resolve lt_le_S blt_lt bge_le : ld.

      Lemma lift1_free: (hds:?; i:?; t:?)
                        (lift1 hds (lift (S i) (0) t)) =
                        (lift (S (trans hds i)) (0) (lift1 (ptrans hds i) t)).
      Proof.
      XElim hds; Simpl.
(* case 1: PNil *)
      XAuto.
(* case 2: PCons *)
      Intros h d hds; Intros; Rewrite H; Clear H; XInduction '(blt (trans hds i) d).
(* case 1: (trans hds i) < d *)
      Pattern 1 d; Rewrite (le_plus_minus (S (trans hds i)) d); Try Rewrite lift_d; XAuto.
(* case 2: (trans hds i) >= d *)
      Rewrite lift_free; Try (Rewrite <- plus_n_Sm; Rewrite plus_sym); XAuto.
      Qed.

   End ptrans_props.