notational change for lsubr:

now looks like the other refinements for local environments

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index ccfa7901101fbe13f2de5f735ff41e3403ad812f..228f9450ca03d78c45e5b1cff46d39eeb005a987 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -60,7 +60,7 @@ lemma cprs_strap2: ∀L,T1,T,T2.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
 lemma cprs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
-                        â\88\80L2. L2 â\89¼ [0, |L1|] L1 → L2 ⊢ T1 ➡* T2.
+                        â\88\80L2. L2 â\8a\91 [0, |L1|] L1 → L2 ⊢ T1 ➡* T2.
 /3 width=3/
 qed.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
index 8df6fb7108c6cb26903451744c15d2422248aa00..fe0359314871b2f07743b23b78d6888de208e2c8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
@@ -101,11 +101,11 @@ lemma lsubsv_fwd_lsubss: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → h ⊢ L1 •⊑[
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=6/
 qed-.
 
-lemma lsubsv_fwd_lsubr1: â\88\80h,g,L1,L2. h â\8a¢ L1 ¡â\8a\91[g] L2 â\86\92 L1 â\89¼[0, |L1|] L2.
+lemma lsubsv_fwd_lsubr1: â\88\80h,g,L1,L2. h â\8a¢ L1 ¡â\8a\91[g] L2 â\86\92 L1 â\8a\91[0, |L1|] L2.
 /3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubr1/
 qed-.
 
-lemma lsubsv_fwd_lsubr2: â\88\80h,g,L1,L2. h â\8a¢ L1 ¡â\8a\91[g] L2 â\86\92 L1 â\89¼[0, |L2|] L2.
+lemma lsubsv_fwd_lsubr2: â\88\80h,g,L1,L2. h â\8a¢ L1 ¡â\8a\91[g] L2 â\86\92 L1 â\8a\91[0, |L2|] L2.
 /3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubr2/
 qed-.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
index cbc1ea3dae57f36f43bd54e43fbdd6b83d2f1c58..5d0643879222d84699730f62cc7da522da803156 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
@@ -165,7 +165,7 @@ lemma cpcs_beta_dx_tpr_rev: ∀a,L,V1,V2,W,T1,T2.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
 lemma cpcs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
-                        â\88\80L2. L2 â\89¼ [0, |L1|] L1 → L2 ⊢ T1 ⬌* T2.
+                        â\88\80L2. L2 â\8a\91 [0, |L1|] L1 → L2 ⊢ T1 ⬌* T2.
 #L1 #T1 #T2 #HT12
 elim (cpcs_inv_cprs … HT12) -HT12
 /3 width=5 by cprs_div, cprs_lsubr_trans/ (**) (* /3 width=5/ is a bit slow *)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma
index ac8f5373cd7163fad79c7ad61cc429f92cc8c92d..364f06adeb2dad43d5e284c2468a8ca8442eae88 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma
@@ -94,11 +94,11 @@ lemma lsubss_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 •⊑[g] K2. ⓑ{I} W2 →
 
 (* Basic_forward lemmas *****************************************************)
 
-lemma lsubss_fwd_lsubr1: â\88\80h,g,L1,L2. h â\8a¢ L1 â\80¢â\8a\91[g] L2 â\86\92 L1 â\89¼[0, |L1|] L2.
+lemma lsubss_fwd_lsubr1: â\88\80h,g,L1,L2. h â\8a¢ L1 â\80¢â\8a\91[g] L2 â\86\92 L1 â\8a\91[0, |L1|] L2.
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
 qed-.
 
-lemma lsubss_fwd_lsubr2: â\88\80h,g,L1,L2. h â\8a¢ L1 â\80¢â\8a\91[g] L2 â\86\92 L1 â\89¼[0, |L2|] L2.
+lemma lsubss_fwd_lsubr2: â\88\80h,g,L1,L2. h â\8a¢ L1 â\80¢â\8a\91[g] L2 â\86\92 L1 â\8a\91[0, |L2|] L2.
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
 qed-.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index 8745932e9d6678a206e06ad84bce8b62bf4fb1a0..de8221468ea0cb24428687200da44e4b83b19c01 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -146,7 +146,7 @@ notation "hvbox( ⇧ [ term 46 d , break term 46 e ] break term 46 T1 ≡ break
    non associative with precedence 45
    for @{ 'RLift $d $e $T1 $T2 }.
 
-notation "hvbox( T1 break â\89¼ [ term 46 d , break term 46 e ] break term 46 T2 )"
+notation "hvbox( T1 break â\8a\91 [ term 46 d , break term 46 e ] break term 46 T2 )"
    non associative with precedence 45
    for @{ 'SubEq $T1 $d $e $T2 }.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
index 2317250cccbb17c8e5c37041c2828a5c6b942f86..d82299c382dbe0d02ffa948fa60f5d1ad396e198 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
@@ -55,7 +55,7 @@ qed.
 (* Note: it does not hold replacing |L1| with |L2| *)
 (* Basic_1: was only: pr2_change *)
 lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
-                       â\88\80L2. L2 â\89¼ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
+                       â\88\80L2. L2 â\8a\91 [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
 #L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
 lapply (tpss_lsubr_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/
 qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
index 7e7ac3c5402105189a651cbc26844198c360c1e8..f1bc18f7dca94106718cc364bece6b01fcac8311 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
@@ -186,10 +186,10 @@ lemma ldrop_O1_lt: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
 ]
 qed.
 
-lemma ldrop_lsubr_ldrop2_abbr: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 →
+lemma ldrop_lsubr_ldrop2_abbr: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 →
                                ∀K2,V,i. ⇩[0, i] L2 ≡ K2. ⓓV →
                                d ≤ i → i < d + e →
-                               â\88\83â\88\83K1. K1 â\89¼ [0, d + e - i - 1] K2 &
+                               â\88\83â\88\83K1. K1 â\8a\91 [0, d + e - i - 1] K2 &
                                      ⇩[0, i] L1 ≡ K1. ⓓV.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e
 [ #d #e #K1 #V #i #H

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
index 2a4e4327186d2822a5acfb39e45df21dee137c2c..89359533aafe83615077962f65f5561a398a0e93 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
@@ -33,35 +33,35 @@ interpretation
 
 definition lsubr_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R.
                         ∀L2,s1,s2. R L2 s1 s2 →
-                        â\88\80L1,d,e. L1 â\89¼ [d, e] L2 → R L1 s1 s2.
+                        â\88\80L1,d,e. L1 â\8a\91 [d, e] L2 → R L1 s1 s2.
 
 (* Basic properties *********************************************************)
 
-lemma lsubr_bind_eq: â\88\80L1,L2,e. L1 â\89¼ [0, e] L2 → ∀I,V.
-                     L1. â\93\91{I} V â\89¼ [0, e + 1] L2.ⓑ{I} V.
+lemma lsubr_bind_eq: â\88\80L1,L2,e. L1 â\8a\91 [0, e] L2 → ∀I,V.
+                     L1. â\93\91{I} V â\8a\91 [0, e + 1] L2.ⓑ{I} V.
 #L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
 qed.
 
-lemma lsubr_abbr_lt: â\88\80L1,L2,V,e. L1 â\89¼ [0, e - 1] L2 → 0 < e →
-                     L1. â\93\93V â\89¼ [0, e] L2.ⓓV.
+lemma lsubr_abbr_lt: â\88\80L1,L2,V,e. L1 â\8a\91 [0, e - 1] L2 → 0 < e →
+                     L1. â\93\93V â\8a\91 [0, e] L2.ⓓV.
 #L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
 qed.
 
-lemma lsubr_abst_lt: â\88\80L1,L2,I,V1,V2,e. L1 â\89¼ [0, e - 1] L2 → 0 < e →
-                     L1. â\93\91{I}V1 â\89¼ [0, e] L2. ⓛV2.
+lemma lsubr_abst_lt: â\88\80L1,L2,I,V1,V2,e. L1 â\8a\91 [0, e - 1] L2 → 0 < e →
+                     L1. â\93\91{I}V1 â\8a\91 [0, e] L2. ⓛV2.
 #L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
 qed.
 
-lemma lsubr_skip_lt: â\88\80L1,L2,d,e. L1 â\89¼ [d - 1, e] L2 → 0 < d →
-                     â\88\80I1,I2,V1,V2. L1. â\93\91{I1} V1 â\89¼ [d, e] L2. ⓑ{I2} V2.
+lemma lsubr_skip_lt: â\88\80L1,L2,d,e. L1 â\8a\91 [d - 1, e] L2 → 0 < d →
+                     â\88\80I1,I2,V1,V2. L1. â\93\91{I1} V1 â\8a\91 [d, e] L2. ⓑ{I2} V2.
 #L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
 qed.
 
-lemma lsubr_bind_lt: â\88\80I,L1,L2,V,e. L1 â\89¼ [0, e - 1] L2 → 0 < e →
-                     L1. â\93\93V â\89¼ [0, e] L2. ⓑ{I}V.
+lemma lsubr_bind_lt: â\88\80I,L1,L2,V,e. L1 â\8a\91 [0, e - 1] L2 → 0 < e →
+                     L1. â\93\93V â\8a\91 [0, e] L2. ⓑ{I}V.
 * /2 width=1/ qed.
 
-lemma lsubr_refl: â\88\80d,e,L. L â\89¼ [d, e] L.
+lemma lsubr_refl: â\88\80d,e,L. L â\8a\91 [d, e] L.
 #d elim d -d
 [ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/
 | #d #IHd #e #L elim L -L // /2 width=1/
@@ -78,7 +78,7 @@ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lsubr_inv_atom1_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 → L1 = ⋆ →
+fact lsubr_inv_atom1_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 → L1 = ⋆ →
                           L2 = ⋆ ∨ (d = 0 ∧ e = 0).
 #L1 #L2 #d #e * -L1 -L2 -d -e
 [ /2 width=1/
@@ -89,13 +89,13 @@ fact lsubr_inv_atom1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L1 = ⋆ →
 ]
 qed.
 
-lemma lsubr_inv_atom1: â\88\80L2,d,e. â\8b\86 â\89¼ [d, e] L2 →
+lemma lsubr_inv_atom1: â\88\80L2,d,e. â\8b\86 â\8a\91 [d, e] L2 →
                        L2 = ⋆ ∨ (d = 0 ∧ e = 0).
 /2 width=3/ qed-.
 
-fact lsubr_inv_skip1_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 →
+fact lsubr_inv_skip1_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 →
                           ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
-                          â\88\83â\88\83I2,K2,V2. K1 â\89¼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+                          â\88\83â\88\83I2,K2,V2. K1 â\8a\91 [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
 #L1 #L2 #d #e * -L1 -L2 -d -e
 [ #d #e #I1 #K1 #V1 #H destruct
 | #L1 #L2 #I1 #K1 #V1 #_ #H
@@ -108,11 +108,11 @@ fact lsubr_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubr_inv_skip1: â\88\80I1,K1,L2,V1,d,e. K1.â\93\91{I1}V1 â\89¼ [d, e] L2 → 0 < d →
-                       â\88\83â\88\83I2,K2,V2. K1 â\89¼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+lemma lsubr_inv_skip1: â\88\80I1,K1,L2,V1,d,e. K1.â\93\91{I1}V1 â\8a\91 [d, e] L2 → 0 < d →
+                       â\88\83â\88\83I2,K2,V2. K1 â\8a\91 [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
 /2 width=5/ qed-.
 
-fact lsubr_inv_atom2_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 → L2 = ⋆ →
+fact lsubr_inv_atom2_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 → L2 = ⋆ →
                           L1 = ⋆ ∨ (d = 0 ∧ e = 0).
 #L1 #L2 #d #e * -L1 -L2 -d -e
 [ /2 width=1/
@@ -123,13 +123,13 @@ fact lsubr_inv_atom2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L2 = ⋆ →
 ]
 qed.
 
-lemma lsubr_inv_atom2: â\88\80L1,d,e. L1 â\89¼ [d, e] ⋆ →
+lemma lsubr_inv_atom2: â\88\80L1,d,e. L1 â\8a\91 [d, e] ⋆ →
                        L1 = ⋆ ∨ (d = 0 ∧ e = 0).
 /2 width=3/ qed-.
 
-fact lsubr_inv_abbr2_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 →
+fact lsubr_inv_abbr2_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 →
                           ∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e →
-                          â\88\83â\88\83K1. K1 â\89¼ [0, e - 1] K2 & L1 = K1.ⓓV.
+                          â\88\83â\88\83K1. K1 â\8a\91 [0, e - 1] K2 & L1 = K1.ⓓV.
 #L1 #L2 #d #e * -L1 -L2 -d -e
 [ #d #e #K1 #V #H destruct
 | #L1 #L2 #K1 #V #_ #_ #H
@@ -140,13 +140,13 @@ fact lsubr_inv_abbr2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubr_inv_abbr2: â\88\80L1,K2,V,e. L1 â\89¼ [0, e] K2.ⓓV → 0 < e →
-                       â\88\83â\88\83K1. K1 â\89¼ [0, e - 1] K2 & L1 = K1.ⓓV.
+lemma lsubr_inv_abbr2: â\88\80L1,K2,V,e. L1 â\8a\91 [0, e] K2.ⓓV → 0 < e →
+                       â\88\83â\88\83K1. K1 â\8a\91 [0, e - 1] K2 & L1 = K1.ⓓV.
 /2 width=5/ qed-.
 
-fact lsubr_inv_skip2_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 →
+fact lsubr_inv_skip2_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 →
                           ∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d →
-                          â\88\83â\88\83I1,K1,V1. K1 â\89¼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
+                          â\88\83â\88\83I1,K1,V1. K1 â\8a\91 [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
 #L1 #L2 #d #e * -L1 -L2 -d -e
 [ #d #e #I1 #K1 #V1 #H destruct
 | #L1 #L2 #I1 #K1 #V1 #_ #H
@@ -159,13 +159,13 @@ fact lsubr_inv_skip2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubr_inv_skip2: â\88\80I2,L1,K2,V2,d,e. L1 â\89¼ [d, e] K2.ⓑ{I2}V2 → 0 < d →
-                       â\88\83â\88\83I1,K1,V1. K1 â\89¼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
+lemma lsubr_inv_skip2: â\88\80I2,L1,K2,V2,d,e. L1 â\8a\91 [d, e] K2.ⓑ{I2}V2 → 0 < d →
+                       â\88\83â\88\83I1,K1,V1. K1 â\8a\91 [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
 /2 width=5/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-fact lsubr_fwd_length_full1_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 →
+fact lsubr_fwd_length_full1_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 →
                                  d = 0 → e = |L1| → |L1| ≤ |L2|.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
 [ //
@@ -176,10 +176,10 @@ fact lsubr_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubr_fwd_length_full1: â\88\80L1,L2. L1 â\89¼ [0, |L1|] L2 → |L1| ≤ |L2|.
+lemma lsubr_fwd_length_full1: â\88\80L1,L2. L1 â\8a\91 [0, |L1|] L2 → |L1| ≤ |L2|.
 /2 width=5/ qed-.
 
-fact lsubr_fwd_length_full2_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 →
+fact lsubr_fwd_length_full2_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 →
                                  d = 0 → e = |L2| → |L2| ≤ |L1|.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
 [ //
@@ -190,5 +190,5 @@ fact lsubr_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubr_fwd_length_full2: â\88\80L1,L2. L1 â\89¼ [0, |L2|] L2 → |L2| ≤ |L1|.
+lemma lsubr_fwd_length_full2: â\88\80L1,L2. L1 â\8a\91 [0, |L2|] L2 → |L2| ≤ |L1|.
 /2 width=5/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
index ebce56c24e30c900fe9c043215a667dcb834d20f..af450e34df23c26043d8dbf39657fefc65fac4fe 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
@@ -34,7 +34,7 @@ interpretation "parallel substritution (term)"
 (* Basic properties *********************************************************)
 
 lemma tps_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 →
-                       â\88\80L2. L2 â\89¼ [d, e] L1 → L2 ⊢ T1 ▶ [d, e] T2.
+                       â\88\80L2. L2 â\8a\91 [d, e] L1 → L2 ⊢ T1 ▶ [d, e] T2.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
 [ //
 | #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma
index e0c736440f4503e41a284c6bad0b138a6bbb7d29..95284abc7f4011c56ced4ecfe07aa35000561d4a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma
@@ -32,7 +32,7 @@ lemma delift_refl_O2: ∀L,T,d. L ⊢ ▼*[d, 0] T ≡ T.
 /2 width=3/ qed.
 
 lemma delift_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼*[d, e] T1 ≡ T2 →
-                          â\88\80L2. L2 â\89¼ [d, e] L1 → L2 ⊢ ▼*[d, e] T1 ≡ T2.
+                          â\88\80L2. L2 â\8a\91 [d, e] L1 → L2 ⊢ ▼*[d, e] T1 ≡ T2.
 #L1 #T1 #T2 #d #e * /3 width=3/
 qed.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
index 10657d3c343bfac077eaa49f5e5f1209d6715f09..b9322cd1eb91571ee5b479ac9749f3695a5355a6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
@@ -39,7 +39,7 @@ interpretation "inverse basic relocation (term) alternative"
 (* Basic properties *********************************************************)
 
 lemma delifta_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
-                           â\88\80L2. L2 â\89¼ [d, e] L1 → L2 ⊢ ▼▼*[d, e] T1 ≡ T2.
+                           â\88\80L2. L2 â\8a\91 [d, e] L1 → L2 ⊢ ▼▼*[d, e] T1 ≡ T2.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/
 [ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
   elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
index d2ce11a36e44219a0030b89e3ed7f27a1947a362..1fdae13f466e93d3bcfe9d12e412b8d54a9206ed 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
@@ -52,7 +52,7 @@ lemma tpss_strap2: ∀L,T1,T,T2,d,e.
 /2 width=3/ qed.
 
 lemma tpss_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
-                        â\88\80L2. L2 â\89¼ [d, e] L1 → L2 ⊢ T1 ▶* [d, e] T2.
+                        â\88\80L2. L2 â\8a\91 [d, e] L1 → L2 ⊢ T1 ▶* [d, e] T2.
 /3 width=3/ qed.
 
 lemma tpss_refl: ∀d,e,L,T. L ⊢ T ▶* [d, e] T.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
index 8adea69bc85923fa5beb183f04753632b65ea823..6fe188a7c1adfa370a4bd705b59445b558a3fa9e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
@@ -36,7 +36,7 @@ interpretation "parallel unfold (term) alternative"
 (* Basic properties *********************************************************)
 
 lemma tpssa_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 →
-                         â\88\80L2. L2 â\89¼ [d, e] L1 → L2 ⊢ T1 ▶▶* [d, e] T2.
+                         â\88\80L2. L2 â\8a\91 [d, e] L1 → L2 ⊢ T1 ▶▶* [d, e] T2.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
 [ //
 | #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 4139f7344348c7090470b74ad3a9daebffb7c187..7ebbbca7f0db5aef1a3becb48128550258d7175e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -239,7 +239,7 @@ table {
           }
         ]
         [ { "local env. ref. for substitution" * } {
-             [ "lsubr ( ? â\89¼[?,?] ? )" "(lsubr_lsubr)" "lsubr_sfr ( ≽[?,?] ? )" * ]
+             [ "lsubr ( ? â\8a\91[?,?] ? )" "(lsubr_lsubr)" "lsubr_sfr ( ≽[?,?] ? )" * ]
           }
         ]
         [ { "restricted structural predecessor for closures" * } {