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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v
index 4e26ce7ea..42f03f2ab 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v
@@ -15,8 +15,8 @@ Require pc3_props.
                              (x1:?) (subst1 d u t1 (lift (1) d x1)) ->
                              (x2:?) (subst1 d u t2 (lift (1) d x2)) ->
                              (pc3 a x1 x2).
-      Intros; Pc3Confluence; Repeat Pr3GenContext.
-      Subst1Confluence; Rewrite H in H3; Clear H x3; XEAuto.
+      Intros; Pc3Unfold; Repeat Pr3GenContext.
+      Subst1Confluence; Rewrite H3 in H5; Clear H3 x3; XEAuto.
       Qed.
 
    End pc3_gen_context.