X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfeq_fqup.ma;h=92479a038daaa25d12f5245de19949ae453cdd61;hb=5c186c72f508da0849058afeecc6877cd9ed6303;hp=bb513ab37528dea116fce5c53cc0930bfedc0689;hpb=e39d1924cd572acdf0cf8dba08f3b650dfd6abee;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma
index bb513ab37..92479a038 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma
@@ -15,9 +15,10 @@
 include "basic_2/static/lfxs_fqup.ma".
 include "basic_2/static/lfeq.ma".
 
-(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *******************)
+(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
 
 (* Advanced properties ******************************************************)
 
+(* Basic_2A1: was: lleq_refl *)
 lemma lfeq_refl: ∀T. reflexive … (lfeq T).
 /2 width=1 by lfxs_refl/ qed.