notational update in ground_2 and basic_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..5daeedab0ca117b1c0f2aa392549e767bede594d 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).
@@ -84,7 +84,7 @@ lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⪤*[R, #0] Y2 →
 ]
 qed-.
 
-lemma lfxs_inv_lref: â\88\80R,Y1,Y2,i. Y1 ⪤*[R, #⫯i] Y2 →
+lemma lfxs_inv_lref: â\88\80R,Y1,Y2,i. Y1 ⪤*[R, #â\86\91i] Y2 →
                      ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
                       | ∃∃I1,I2,L1,L2. L1 ⪤*[R, #i] L2 &
                                        Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
@@ -183,7 +183,7 @@ lemma lfxs_inv_zero_unit_dx: ∀R,I,L1,K2. L1 ⪤*[R, #0] K2.ⓤ{I} →
 ]
 qed-.
 
-lemma lfxs_inv_lref_bind_sn: â\88\80R,I1,K1,L2,i. K1.â\93\98{I1} ⪤*[R, #⫯i] L2 →
+lemma lfxs_inv_lref_bind_sn: â\88\80R,I1,K1,L2,i. K1.â\93\98{I1} ⪤*[R, #â\86\91i] L2 →
                              ∃∃I2,K2. K1 ⪤*[R, #i] K2 & L2 = K2.ⓘ{I2}.
 #R #I1 #K1 #L2 #i #H elim (lfxs_inv_lref … H) -H *
 [ #H destruct
@@ -191,7 +191,7 @@ lemma lfxs_inv_lref_bind_sn: ∀R,I1,K1,L2,i. K1.ⓘ{I1} ⪤*[R, #⫯i] L2 →
 ]
 qed-.
 
-lemma lfxs_inv_lref_bind_dx: â\88\80R,I2,K2,L1,i. L1 ⪤*[R, #⫯i] K2.ⓘ{I2} →
+lemma lfxs_inv_lref_bind_dx: â\88\80R,I2,K2,L1,i. L1 ⪤*[R, #â\86\91i] K2.ⓘ{I2} →
                              ∃∃I1,K1. K1 ⪤*[R, #i] K2 & L1 = K1.ⓘ{I1}.
 #R #I2 #K2 #L1 #i #H elim (lfxs_inv_lref … H) -H *
 [ #_ #H destruct
@@ -273,7 +273,7 @@ lemma lfxs_unit: ∀R,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cext2 R, cfull, f] L2 
 /4 width=3 by frees_unit, lexs_next, ext2_unit, ex2_intro/ qed.
 
 lemma lfxs_lref: ∀R,I1,I2,L1,L2,i.
-                 L1 ⪤*[R, #i] L2 â\86\92 L1.â\93\98{I1} ⪤*[R, #⫯i] L2.ⓘ{I2}.
+                 L1 ⪤*[R, #i] L2 â\86\92 L1.â\93\98{I1} ⪤*[R, #â\86\91i] L2.ⓘ{I2}.
 #R #I1 #I2 #L1 #L2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/
 qed.
 
@@ -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/