(****************************************************************************)
(*                                                                          *)
(*                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 lift1_defs.

   Section lift1_props. (****************************************************)

      Lemma lift1_xhg: (hds:?; t:?)
                       (lift1 (Ss hds) (lift (1) (0) t)) =
                       (lift (1) (0) (lift1 hds t)).
      Proof.
      XElim hds.
(* case 1: PNil *)
      Intros; Simpl; XAuto.
(* case 2: PCons *)
      Intros h d; Simpl; Intros.
      Rewrite H; Clear H.
      Arith0 d; Rewrite lift_d; XAuto.
      Qed.

   End lift1_props.

   Section lifts1_props. (***************************************************)

      Lemma lifts1_xhg: (hds:?; ts:?)
                        (lifts1 (Ss hds) (lifts (1) (0) ts)) =
                        (lifts (1) (0) (lifts1 hds ts)).
      Proof.
      Intros; XElim ts; Simpl; Intros;
      Try Rewrite lift1_xhg; Try Rewrite H; XAuto.
      Qed.

   End lifts1_props.