Require lift_props.
Require subst0_lift.
Require pr0_defs.

(*#* #caption "main properties of predicate \\texttt{pr0}" *)
(*#* #clauses pr0_props *)

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

(*#* #caption "conguence with lift" *)
(*#* #cap #cap t1,t2 #alpha d in i *)

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

(*#* #stop file *)

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

   End pr0_lift.

      Hints Resolve pr0_lift : ltlc.