X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Flift_defs.v;h=8b69ec4b49c62cb3c639e182bd8c8c3990b8f20a;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=1f61d9fadaf75afdc6ea79d20019d847953fb365;hpb=50cfabb6b8136873a02f8fd1512f0b62f97e2639;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v b/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v
index 1f61d9fad..8b69ec4b4 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v
@@ -183,7 +183,9 @@ Require Export terms_defs.
             | [ H1: (le ?1 ?2); H2: (lt ?2 (plus ?1 ?3));
                 H3: (TLRef ?2) = (lift ?3 ?1 ?4) |- ? ] ->
                Apply (lift_gen_lref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto
-            | [ H: (TLRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
+            | [ _: (TLRef ?1) = (lift (S ?1) (0) ?2) |- ? ] ->
+	       EApply lift_gen_lref_false; [ Idtac | Idtac | XEAuto ]; XEAuto
+	    | [ H: (TLRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
                LApply (lift_gen_lref_false (1) ?1 ?1); [ Intros H_x | XAuto ];
                LApply H_x; [ Clear H_x; Intros H_x | Arith7' ?1; XAuto ];
                LApply (H_x ?2); [ Clear H_x; Intros H_x | XAuto ];