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 f3f64b5ffe15c55941823c8a885e99c4c14bb15e..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).
@@ -38,7 +38,7 @@ definition lfxs_confluent: relation … ≝
                            ∀K1,K,V1. K1 ⪤*[R1, V1] K → ∀V. R1 K1 V1 V →
                            ∀K2. K ⪤*[R2, V] K2 → K ⪤*[R2, V1] K2.
 
-definition lfxs_transitive: relation3 ? (relation3 ?? term) ? ≝
+definition lfxs_transitive: relation3 ? (relation3 ?? term) … ≝
                             λR1,R2,R3.
                             ∀K1,K,V1. K1 ⪤*[R1, V1] K →
                             ∀V. R1 K1 V1 V → ∀V2. R2 K V V2 → R3 K1 V1 V2.
@@ -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/