update in basic_2 and ground_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index f2ab35f91a30c403f9948b99c2956341e66b7e08..8d82750f1db9f679e65824f307e5f1e4abfe4a6e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -21,7 +21,7 @@ include "basic_2/static/frees.ma".
 (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
 
 definition lfxs (R) (T): relation lenv ≝
-                λL1,L2. â\88\83â\88\83f. L1 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f & L1 ⪤*[cext2 R, cfull, f] L2.
+                λL1,L2. â\88\83â\88\83f. L1 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f & L1 ⪤*[cext2 R, cfull, f] L2.
 
 interpretation "generic extension on referred entries (local environment)"
    'RelationStar R T L1 L2 = (lfxs R T L1 L2).
@@ -300,8 +300,8 @@ lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
 qed-.
 
 lemma lfxs_isid: ∀R1,R2,L1,L2,T1,T2.
-                 (â\88\80f. L1 â\8a¢ ð\9d\90\85*â¦\83T1â¦\84 â\89¡ f → 𝐈⦃f⦄) →
-                 (â\88\80f. ð\9d\90\88â¦\83fâ¦\84 â\86\92 L1 â\8a¢ ð\9d\90\85*â¦\83T2â¦\84 â\89¡ f) →
+                 (â\88\80f. L1 â\8a¢ ð\9d\90\85*â¦\83T1â¦\84 â\89\98 f → 𝐈⦃f⦄) →
+                 (â\88\80f. ð\9d\90\88â¦\83fâ¦\84 â\86\92 L1 â\8a¢ ð\9d\90\85*â¦\83T2â¦\84 â\89\98 f) →
                  L1 ⪤*[R1, T1] L2 → L1 ⪤*[R2, T2] L2.
 #R1 #R2 #L1 #L2 #T1 #T2 #H1 #H2 *
 /4 width=7 by lexs_co_isid, ex2_intro/