X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfxs_lex.ma;h=2957ac1c3460d3c10c86a753533866fcba250952;hp=01f578f4eb581a764f2436e6f75bfa99604cb4ff;hb=268e7f336d036f77ffc9663358e9afda92b97730;hpb=1604f2ee65c57eefb7c6b3122eab2a9f32e0552d

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma
index 01f578f4e..2957ac1c3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma
@@ -31,7 +31,7 @@ qed.
 lemma lfxs_inv_lex_lfeq: ∀R. c_reflexive … R →
                          lfxs_fsge_compatible R →
                          ∀L1,L2,T. L1 ⪤*[R, T] L2 →
-                         ∃∃L. L1 ⪤[R] L & L ≡[T] L2.
+                         ∃∃L. L1 ⪤[R] L & L ≐[T] L2.
 #R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL
 elim (lexs_sdj_split … ceq_ext … HL 𝐈𝐝 ?) -HL
 [ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] -H1R