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

Require subst0_lift.
Require getl_props.
Require pr0_lift.
Require pr2_defs.

   Section pr2_lift. (*******************************************************)

      Hints Resolve le_S_n : ld.

      Lemma pr2_lift: (c,e:?; h,d:?) (drop h d c e) ->
                      (t1,t2:?) (pr2 e t1 t2) ->
                      (pr2 c (lift h d t1) (lift h d t2)).
      Proof.
      Intros until 2; InsertEq H0 e; XElim H0; Clear y t1 t2.
(* case 1 : pr2_free *)
      XAuto.
(* case 2 : pr2_delta *)
      Intros; Subst; Apply (lt_le_e i d); Intros; GetLDis.
(* case 2.1 : i < d *)
      Rewrite minus_x_Sy in H0; [ Idtac | XAuto ].
      DropClear; XDEAuto 5.
(* case 2.2 : i >= d *)
      XDEAuto 4.
      Qed.

   End pr2_lift.

      Hints Resolve pr2_lift : ld.