X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Ftheq_tdeq.ma;h=b70559d87e370f87503509a04e888c27d982395f;hp=99447dba76fb81f08daace0c7ed5c7158f38ee23;hb=4173283e148199871d787c53c0301891deb90713;hpb=a67fc50ccfda64377e2c94c18c3a0d9265f651db

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/theq_tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/theq_tdeq.ma
index 99447dba7..b70559d87 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/theq_tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/theq_tdeq.ma
@@ -17,8 +17,8 @@ include "static_2/syntax/theq.ma".
 
 (* HEAD EQUIVALENCE FOR TERMS ***********************************************)
 
-(* Properties with degree-based equivalence for terms ***********************)
+(* Properties with sort-irrelevant equivalence for terms ********************)
 
-lemma tdeq_theq: ∀h,o,T1,T2. T1 ≛[h, o] T2 → T1 ⩳[h, o] T2.
-#h #o #T1 #T2 * -T1 -T2 /2 width=3 by theq_sort, theq_pair/
+lemma tdeq_theq: ∀T1,T2. T1 ≛ T2 → T1 ⩳ T2.
+#T1 #T2 * -T1 -T2 /2 width=1 by theq_sort, theq_pair/
 qed.