renaming

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfeq_fqup.ma

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 bb513ab37528dea116fce5c53cc0930bfedc0689..92479a038daaa25d12f5245de19949ae453cdd61 100644 (file)
--- 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.