X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr0_lift.v;h=b6d9ba247c821442afc65f059ff42353e6816f57;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=f3dc1c5184dde691ed7b6a338a871a2d653da410;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v
index f3dc1c518..b6d9ba247 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v
@@ -2,9 +2,11 @@ Require lift_props.
 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" *)
@@ -13,8 +15,6 @@ Require pr0_defs.
       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.
@@ -22,7 +22,7 @@ Require pr0_defs.
       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.