6 (*#* #caption "main properties of predicate \\texttt{pr2}" *)
7 (*#* #clauses pr2_props *)
9 Section pr2_lift. (*******************************************************)
11 (*#* #caption "conguence with lift" *)
12 (*#* #cap #cap c, t1, t2 #alpha e in D, d in i *)
14 Theorem pr2_lift : (c,e:?; h,d:?) (drop h d c e) ->
15 (t1,t2:?) (pr2 e t1 t2) ->
16 (pr2 c (lift h d t1) (lift h d t2)).
20 Intros until 2; XElim H0; Intros.
21 (* case 1 : pr2_pr0 *)
23 (* case 2 : pr2_delta *)
24 Apply (lt_le_e i d); Intros; DropDis.
25 (* case 2.1 : i < d *)
26 Rewrite minus_x_Sy in H0; [ Idtac | XAuto ].
27 DropGenBase; Rewrite H0 in H; Simpl in H; XEAuto.
28 (* case 2.2 : i >= d *)
34 Hints Resolve pr2_lift : ltlc.