Require subst0_lift.
Require pr0_defs.
-(*#* #caption "main properties of predicate \\texttt{pr0}" *)
+(*#* #caption "main properties of the relation $\\PrZ{}{}$" *)
(*#* #clauses pr0_props *)
+(*#* #stop file *)
+
Section pr0_lift. (*******************************************************)
(*#* #caption "conguence with lift" *)
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.
LiftTailRw; XAuto.
(* case 3 : pr0_beta *)
LiftTailRw; XAuto.
-(* case 4: pr0_gamma *)
+(* case 4: pr0_upsilon *)
LiftTailRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
(* case 5: pr0_delta *)
LiftTailRw; Simpl.