milestone in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / rdeq_req.ma

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 ab3ebca9886a9233688001da30f8f48f11750404..5ef8bef9b99598b1fbf6535804815eaeb393225a 100644 (file)
--- 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-.