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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v
index 9f828bfa8..3546cb5f2 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v
@@ -1,3 +1,5 @@
+(*#* #stop file *)
+
 Require subst0_lift.
 Require drop_props.
 Require pr0_lift.
@@ -14,11 +16,8 @@ Require pr2_defs.
       Theorem pr2_lift : (c,e:?; h,d:?) (drop h d c e) ->
                          (t1,t2:?) (pr2 e t1 t2) ->
                          (pr2 c (lift h d t1) (lift h d t2)).
-
-(*#* #stop file *)
-
       Intros until 2; XElim H0; Intros.
-(* case 1 : pr2_pr0 *)
+(* case 1 : pr2_free *)
       XAuto.
 (* case 2 : pr2_delta *)
       Apply (lt_le_e i d); Intros; DropDis.