update in basic_2 + web page

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfxs_lex.ma

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 01f578f4eb581a764f2436e6f75bfa99604cb4ff..2957ac1c3460d3c10c86a753533866fcba250952 100644 (file)
--- 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 →
-                         â\88\83â\88\83L. L1 ⪤[R] L & L â\89¡[T] L2.
+                         â\88\83â\88\83L. L1 ⪤[R] L & L â\89\90[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