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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v b/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v
index d1e091348..93e0d2ecf 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v
@@ -32,8 +32,8 @@ Require Export subst0_defs.
       Try Subst0GenBase; XAuto.
       Qed.
 
-      Theorem subst1_gen_bref : (v,x:?; i,n:?) (subst1 i v (TBRef n) x) ->
-                                x = (TBRef n) \/
+      Theorem subst1_gen_lref : (v,x:?; i,n:?) (subst1 i v (TLRef n) x) ->
+                                x = (TLRef n) \/
                                 n = i /\ x = (lift (S n) (0) v).
       Intros; XElim H; Clear x; Intros;
       Try Subst0GenBase; XAuto.