milestone in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / theq_tdeq.ma

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 99447dba76fb81f08daace0c7ed5c7158f38ee23..b70559d87e370f87503509a04e888c27d982395f 100644 (file)
--- 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.