X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Ftheq_tdeq.ma;h=e151e40f0a07dc945685891d14ece5f92f8d5511;hp=2a111b40f191ea4b2a61bacc664eab3a7810889b;hb=222044da28742b24584549ba86b1805a87def070;hpb=69592aa1d0c0d122fb09f11cc53bf4c5a1532fdd

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma
index 2a111b40f..e151e40f0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma
@@ -19,6 +19,6 @@ include "basic_2/syntax/theq.ma".
 
 (* Properties with degree-based equivalence for terms ***********************)
 
-lemma tdeq_theq: ∀h,o,T1,T2. T1 ≡[h, o] T2 → T1 ⩳[h, o] T2.
+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/
 qed.