X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fty0_gen_context.v;fp=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fty0_gen_context.v;h=f04a6aa5e55d007e9fc6daa9585c4e084d826d7c;hb=50cfabb6b8136873a02f8fd1512f0b62f97e2639;hp=bf9217602bead686fbab3e5f6162e8794523ba73;hpb=619a3a478a4f6b0a50782b620009f6a141c30a53;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v
index bf9217602..f04a6aa5e 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v
@@ -53,7 +53,7 @@ Require ty0_lift.
       Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
       Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
       EApply ex3_2_intro;
-      [ Rewrite lift_bref_lt | Rewrite lift_d | EApply ty0_abbr ]; XEAuto.
+      [ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty0_abbr ]; XEAuto.
 (* case 3.2 : n = d0 *)
       Rewrite H7; Rewrite H7 in H0; Clear H2 H7 n.
       DropDis; Inversion H0; Rewrite H8 in H4; Clear H0 H7 H8 e u0.
@@ -67,7 +67,7 @@ Require ty0_lift.
       Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
       Arith4c '(0) '(minus n (1)).
       EApply ex3_2_intro;
-      [ Rewrite lift_bref_ge
+      [ Rewrite lift_lref_ge
       | Rewrite lift_free; Simpl
       | Pattern 2 n; Rewrite (minus_x_SO n)
       ]; XEAuto.
@@ -84,7 +84,7 @@ Require ty0_lift.
       Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
       Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
       EApply ex3_2_intro;
-      [ Rewrite lift_bref_lt | Rewrite lift_d | EApply ty0_abst ]; XEAuto.
+      [ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty0_abst ]; XEAuto.
 (* case 4.2 : n = d0 *)
       Rewrite H7; Rewrite H7 in H0; DropDis; Inversion H0.
 (* case 4.3 : n > d0 *)
@@ -92,7 +92,7 @@ Require ty0_lift.
       Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
       Arith4c '(0) '(minus n (1)).
       EApply ex3_2_intro;
-      [ Rewrite lift_bref_ge
+      [ Rewrite lift_lref_ge
       | Rewrite lift_free; Simpl
       | Pattern 2 n; Rewrite (minus_x_SO n)
       ]; XEAuto.
@@ -149,7 +149,7 @@ Require ty0_lift.
       LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
       Rewrite <- lift_d; [ Idtac | XAuto ].
       Rewrite <- le_plus_minus; [ Idtac | XAuto ].
-      EApply ex3_2_intro; [ Rewrite lift_bref_lt | Idtac | EApply ty0_abbr ]; XEAuto.
+      EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty0_abbr ]; XEAuto.
 (* case 3.2 : n = d0 *)
       Rewrite H6 in H0; DropDis; Inversion H0.
 (* case 3.3 : n > d0 *)
@@ -157,7 +157,7 @@ Require ty0_lift.
       Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
       Arith4c '(0) '(minus n (1)).
       EApply ex3_2_intro;
-      [ Rewrite lift_bref_ge
+      [ Rewrite lift_lref_ge
       | Rewrite lift_free; Simpl
       | Pattern 2 n; Rewrite (minus_x_SO n)
       ]; XEAuto.
@@ -171,7 +171,7 @@ Require ty0_lift.
       LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
       Rewrite <- lift_d; [ Idtac | XAuto ].
       Rewrite <- le_plus_minus; [ Idtac | XAuto ].
-      EApply ex3_2_intro; [ Rewrite lift_bref_lt | Idtac | EApply ty0_abst ]; XEAuto.
+      EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty0_abst ]; XEAuto.
 (* case 4.2 : n = d0 *)
       Rewrite H6 in H0; DropDis; Inversion H0.
 (* case 4.3 : n > d0 *)
@@ -179,7 +179,7 @@ Require ty0_lift.
       Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
       Arith4c '(0) '(minus n (1)).
       EApply ex3_2_intro;
-      [ Rewrite lift_bref_ge
+      [ Rewrite lift_lref_ge
       | Rewrite lift_free; [ Simpl | Simpl | Idtac ]
       | Pattern 2 n; Rewrite (minus_x_SO n)
       ]; XEAuto.