5 (*#* #caption "main properties of the relation $\\PrZ{}{}$" *)
6 (*#* #clauses pr0_props *)
10 Section pr0_lift. (*******************************************************)
12 (*#* #caption "conguence with lift" *)
13 (*#* #cap #cap t1,t2 #alpha d in i *)
15 Theorem pr0_lift: (t1,t2:?) (pr0 t1 t2) ->
16 (h,d:?) (pr0 (lift h d t1) (lift h d t2)).
18 Intros until 1; XElim H; Intros.
19 (* case 1: pr0_refl *)
21 (* case 2: pr0_cong *)
23 (* case 3 : pr0_beta *)
25 (* case 4: pr0_upsilon *)
26 LiftTailRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
27 (* case 5: pr0_delta *)
29 EApply pr0_delta; [ XAuto | Apply H2 | Idtac ].
30 LetTac d' := (S d); Arith10 d; Unfold d'; XAuto.
31 (* case 6: pr0_zeta *)
32 LiftTailRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
33 (* case 7: pr0_epsilon *)
39 Hints Resolve pr0_lift : ltlc.