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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v
index 107a4ca89..ebe6bfcc7 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v
@@ -26,11 +26,11 @@ Require ty0_defs.
 (* case 3.1 : n < d0 *)
       Rewrite minus_x_Sy in H4; [ Idtac | XAuto ].
       DropGenBase; Rewrite H4 in H0; Clear H4 x.
-      Rewrite lift_bref_lt; [ Idtac | XAuto ].
+      Rewrite lift_lref_lt; [ Idtac | XAuto ].
       Arith8 d0 '(S n); Rewrite lift_d; [ Arith8' d0 '(S n) | XAuto ].
       EApply ty0_abbr; XEAuto.
 (* case 3.2 : n >= d0 *)
-      Rewrite lift_bref_ge; [ Idtac | XAuto ].
+      Rewrite lift_lref_ge; [ Idtac | XAuto ].
       Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
       Rewrite (plus_sym h (S n)); Simpl; XEAuto.
 (* case 4: ty0_abst *)
@@ -38,11 +38,11 @@ Require ty0_defs.
 (* case 4.1 : n < d0 *)
       Rewrite minus_x_Sy in H4; [ Idtac | XAuto ].
       DropGenBase; Rewrite H4 in H0; Clear H4 x.
-      Rewrite lift_bref_lt; [ Idtac | XAuto ].
+      Rewrite lift_lref_lt; [ Idtac | XAuto ].
       Arith8 d0 '(S n); Rewrite lift_d; [ Arith8' d0 '(S n) | XAuto ].
       EApply ty0_abst; XEAuto.
 (* case 4.2 : n >= d0 *)
-      Rewrite lift_bref_ge; [ Idtac | XAuto ].
+      Rewrite lift_lref_ge; [ Idtac | XAuto ].
       Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
       Rewrite (plus_sym h (S n)); Simpl; XEAuto.
 (* case 5: ty0_bind *)