some reorganization and some corrections

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / ty0_gen_context.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v
index bf9217602bead686fbab3e5f6162e8794523ba73..f04a6aa5e55d007e9fc6daa9585c4e084d826d7c 100644 (file)
--- 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.