(****************************************************************************)
(*                                                                          *)
(*                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 subst0_lift.
Require pr0_defs.

   Section pr0_lift. (*******************************************************)

      Lemma pr0_lift: (t1,t2:?) (pr0 t1 t2) ->
                      (h,d:?) (pr0 (lift h d t1) (lift h d t2)).

      Proof.
      Intros until 1; XElim H; Clear t1 t2; Intros.
(* case 1: pr0_refl *)
      XAuto.
(* case 2: pr0_cong *)
      LiftHeadRw; XAuto.
(* case 3 : pr0_beta *)
      LiftHeadRw; XAuto.
(* case 4: pr0_upsilon *)
      LiftHeadRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
(* case 5: pr0_delta *)
      LiftHeadRw; Simpl.
      EApply pr0_delta; [ XAuto | Apply H2 | Idtac ].
      LetTac d' := (S d); Arith10 d; Unfold d'; XAuto.
(* case 6: pr0_zeta *)
      LiftHeadRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
(* case 7: pr0_tau *)
      LiftHeadRw; XAuto.
      Qed.

   End pr0_lift.

      Hints Resolve pr0_lift : ld.