5 (*#* #caption "main properties of predicate \\texttt{pr0}" *)
6 (*#* #clauses pr0_props *)
8 Section pr0_lift. (*******************************************************)
10 (*#* #caption "conguence with lift" *)
11 (*#* #cap #cap t1,t2 #alpha d in i *)
13 Theorem pr0_lift: (t1,t2:?) (pr0 t1 t2) ->
14 (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_gamma *)
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.