renaming in basic_2

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

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 2a111b40f191ea4b2a61bacc664eab3a7810889b..e151e40f0a07dc945685891d14ece5f92f8d5511 100644 (file)
--- 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: â\88\80h,o,T1,T2. T1 â\89¡[h, o] T2 → T1 ⩳[h, o] T2.
+lemma tdeq_theq: â\88\80h,o,T1,T2. T1 â\89\9b[h, o] T2 → T1 ⩳[h, o] T2.
 #h #o #T1 #T2 * -T1 -T2 /2 width=3 by theq_sort, theq_pair/
 qed.