X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Frdeq_req.ma;h=5ef8bef9b99598b1fbf6535804815eaeb393225a;hp=ab3ebca9886a9233688001da30f8f48f11750404;hb=4173283e148199871d787c53c0301891deb90713;hpb=a67fc50ccfda64377e2c94c18c3a0d9265f651db

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rdeq_req.ma b/matita/matita/contribs/lambdadelta/static_2/static/rdeq_req.ma
index ab3ebca98..5ef8bef9b 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/rdeq_req.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/rdeq_req.ma
@@ -15,13 +15,13 @@
 include "static_2/static/req_fsle.ma".
 include "static_2/static/rdeq.ma".
 
-(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******)
+(* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***)
 
 (* Properties with syntactic equivalence on referred entries ****************)
 
-lemma req_rdeq: ∀h,o,L1,L2. ∀T:term. L1 ≡[T] L2 → L1 ≛[h, o, T] L2.
+lemma req_rdeq: ∀L1,L2. ∀T:term. L1 ≡[T] L2 → L1 ≛[T] L2.
 /2 width=3 by rex_co/ qed.
 
-lemma req_rdeq_trans: ∀h,o,L1,L. ∀T:term. L1 ≡[T] L →
-                      ∀L2. L ≛[h, o, T] L2 → L1 ≛[h, o, T] L2.
+lemma req_rdeq_trans: ∀L1,L. ∀T:term. L1 ≡[T] L →
+                      ∀L2. L ≛[T] L2 → L1 ≛[T] L2.
 /2 width=3 by req_rex_trans/ qed-.