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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_subst0.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_subst0.v
index ace613d6e..46a137e18 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr0_subst0.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_subst0.v
@@ -41,8 +41,8 @@ Require pr0_lift.
 
 (*#* #start file *)
 
-(*#* #caption "confluence with substitution" *)
-(*#* #cap #cap t1,t2,v1,v2 #alpha w1 in U1, w2 in U2 *)
+(*#* #caption "confluence with strict substitution" *)
+(*#* #cap #cap t1, t2 #alpha v1 in W1, v2 in W2, w1 in U1, w2 in U2 *)
 
       Theorem pr0_subst0: (t1,t2:?) (pr0 t1 t2) ->
                           (v1,w1:?; i:?) (subst0 i v1 t1 w1) ->
@@ -60,7 +60,7 @@ Require pr0_lift.
 (* case 3: pr0_beta *)
       Repeat Subst0Gen; Rewrite H3; Try Rewrite H5; Try Rewrite H6;
       Repeat IH; XEAuto.
-(* case 4: pr0_gamma *)
+(* case 4: pr0_upsilon *)
       Repeat Subst0Gen; Rewrite H6; Try Rewrite H8; Try Rewrite H9;
       Repeat IH; XDEAuto 7.
 (* case 5: pr0_delta *)
@@ -95,10 +95,10 @@ Require pr0_lift.
                LApply (H1 ?4 ?5 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
                LApply (H1 ?4); [ Clear H1; Intros H1 | XAuto ];
                XElim H1; [ Intros | Intros H1; XElim H1; Intros ]
-            | [ H1: (subst0 ?0 ?1 ?2 ?3); H2: (pr0 ?4 ?1) |- ? ] ->
-               LApply (pr0_subst0_back ?1 ?2 ?3 ?0); [ Clear H1; Intros H1 | XAuto ];
-               LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
-               XElim H1; Intros
+            | [ _: (subst0 ?0 ?1 ?2 ?3); _: (pr0 ?4 ?1) |- ? ] ->
+               LApply (pr0_subst0_back ?1 ?2 ?3 ?0); [ Intros H_x | XAuto ];
+               LApply (H_x ?4); [ Clear H_x; Intros H_x | XAuto ];
+               XElim H_x; Intros
             | [ H1: (subst0 ?0 ?1 ?2 ?3); H2: (pr0 ?1 ?4) |- ? ] ->
                LApply (pr0_subst0_fwd ?1 ?2 ?3 ?0); [ Clear H1; Intros H1 | XAuto ];
                LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];