notational change for lsubr:

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / lsubr.ma

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-.