X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr3_props.v;h=106bfe66cab6a2851a247ee4e8b7aa8637e27770;hb=244d65f63ca6a736b871f9f91328fe8c5524ff05;hp=dfdc49c5048de07d3f49c206b10f4c1dcf2b37b5;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v
index dfdc49c50..106bfe66c 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v
@@ -35,7 +35,7 @@ Require pr3_defs.
 (* case 2.1 : i0 = 0 *)
       DropGenBase; Inversion H2; Clear H2.
       Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.
-      Subst0Subst0; Arith9'In H4 i; XDEAuto 7.
+      Subst0Subst0; Arith9'In H4 i. (*; XDEAuto 7.
 (* case 2.2 : i0 > 0 *)
       Clear IHi0; NewInduction k; DropGenBase; XEAuto.
       Qed.
@@ -111,3 +111,4 @@ Require pr3_defs.
 
       Hints Resolve pr3_lift : ltlc.
 
+*)