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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v
index 7a0acfeb6..d46ca3555 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v
@@ -17,14 +17,14 @@ Require subst0_defs.
       XElim t1; Intros.
 (* case 1: TSort *)
       Rewrite lift_sort in H; Subst0GenBase.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
       Apply (lt_le_e n (S (plus i d))); Intros.
 (* case 2.1: n < 1 + i + d *)
-      Rewrite lift_bref_lt in H; [ Idtac | XAuto ].
+      Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
       Subst0GenBase; Rewrite H1; Rewrite H.
       Rewrite <- lift_d; Simpl; XEAuto.
 (* case 2.2: n >= 1 + i + d *)
-      Rewrite lift_bref_ge in H; [ Idtac | XAuto ].
+      Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
       Subst0GenBase; Rewrite <- H in H0.
       EApply le_false; [ Idtac | Apply H0 ]; XAuto.
 (* case 3: TTail k *)
@@ -49,14 +49,14 @@ Require subst0_defs.
       XElim t; Intros.
 (* case 1: TSort *)
       Rewrite lift_sort in H1; Subst0GenBase.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
       Apply (lt_le_e n d); Intros.
 (* case 2.1: n < d *)
-      Rewrite lift_bref_lt in H1; [ Idtac | XAuto ].
+      Rewrite lift_lref_lt in H1; [ Idtac | XAuto ].
       Subst0GenBase; Rewrite H1 in H2.
       EApply le_false; [ Apply H | XAuto ].
 (* case 2.2: n >= d *)
-      Rewrite lift_bref_ge in H1; [ Idtac | XAuto ].
+      Rewrite lift_lref_ge in H1; [ Idtac | XAuto ].
       Subst0GenBase; Rewrite <- H1 in H0.
       EApply le_false; [ Apply H2 | XEAuto ].
 (* case 3: TTail k *)
@@ -87,14 +87,14 @@ Require subst0_defs.
       XElim t1; Intros.
 (* case 1: TSort *)
       Rewrite lift_sort in H; Subst0GenBase.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
       Apply (lt_le_e n d); Intros.
 (* case 2.1: n < d *)
-      Rewrite lift_bref_lt in H; [ Idtac | XAuto ].
+      Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
       Subst0GenBase; Rewrite H in H1.
       EApply le_false; [ Apply H0 | XAuto ].
 (* case 2.2: n >= d *)
-      Rewrite lift_bref_ge in H; [ Idtac | XAuto ].
+      Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
       Subst0GenBase; Rewrite <- H; Rewrite H2.
       Rewrite minus_plus_r.
       EApply ex2_intro; [ Idtac | XAuto ].