X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr0_gen.v;h=bfe189586eccd8980d69d0d5c31fbfad0514aa0a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=0b634e59c8c314a4d90a7ad5817b64f3b0b2ec56;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v
index 0b634e59c..bfe189586 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v
@@ -44,16 +44,11 @@ Require pr0_lift.
                XElim H_x; Intro; Intros H_x; Intro;
                Try Rewrite H_x; Try Rewrite H_x in H3; Clear H_x.
 
-(*#* #start file *)
-
 (*#* #caption "generation lemma for lift" *)
 (*#* #cap #alpha t1 in U1, t2 in U2, x in T, d in i *)
 
       Theorem pr0_gen_lift : (t1,x:?; h,d:?) (pr0 (lift h d t1) x) ->
                              (EX t2 | x = (lift h d t2) & (pr0 t1 t2)).
-
-(*#* #stop file *)
-
       Intros until 1; InsertEq H '(lift h d t1);
       UnIntro H d; UnIntro H t1; XElim H; Clear y x; Intros;
       Rename x into t3; Rename x0 into d.
@@ -66,7 +61,7 @@ Require pr0_lift.
       LiftGen; Rewrite H3; Clear H3 t0.
       LiftGen; Rewrite H3; Clear H3 H5 x1 k.
       IH; IH; XEAuto.
-(* case 4 : pr0_gamma *)
+(* case 4 : pr0_upsilon *)
       LiftGen; Rewrite H6; Clear H6 t0.
       LiftGen; Rewrite H6; Clear H6 x1.
       IH; IH; IH.