renaming in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / drops_length.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma
index 10cc0f5798a38b16b405917c6ac79cf152a47376..7543a555908d738cef29fc8917f313c131c60fc8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma
@@ -20,13 +20,13 @@ include "basic_2/relocation/drops.ma".
 (* Forward lemmas with length for local environments ************************)
 
 (* Basic_2A1: includes: drop_fwd_length_le4 *)
-lemma drops_fwd_length_le4: â\88\80b,f,L1,L2. â¬\87*[b, f] L1 â\89¡ L2 → |L2| ≤ |L1|.
+lemma drops_fwd_length_le4: â\88\80b,f,L1,L2. â¬\87*[b, f] L1 â\89\98 L2 → |L2| ≤ |L1|.
 #b #f #L1 #L2 #H elim H -f -L1 -L2 /2 width=1 by le_S, le_S_S/
 qed-.
 
 (* Basic_2A1: includes: drop_fwd_length_eq1 *)
-theorem drops_fwd_length_eq1: â\88\80b1,b2,f,L1,K1. â¬\87*[b1, f] L1 â\89¡ K1 →
-                              â\88\80L2,K2. â¬\87*[b2, f] L2 â\89¡ K2 →
+theorem drops_fwd_length_eq1: â\88\80b1,b2,f,L1,K1. â¬\87*[b1, f] L1 â\89\98 K1 →
+                              â\88\80L2,K2. â¬\87*[b2, f] L2 â\89\98 K2 →
                               |L1| = |L2| → |K1| = |K2|.
 #b1 #b2 #f #L1 #K1 #HLK1 elim HLK1 -f -L1 -K1
 [ #f #_ #L2 #K2 #HLK2 #H lapply (length_inv_zero_sn … H) -H
@@ -43,8 +43,8 @@ qed-.
 
 (* forward lemmas with finite colength assignment ***************************)
 
-lemma drops_fwd_fcla: â\88\80f,L1,L2. â¬\87*[â\93\89, f] L1 â\89¡ L2 →
-                      â\88\83â\88\83n. ð\9d\90\82â¦\83fâ¦\84 â\89¡ n & |L1| = |L2| + n.
+lemma drops_fwd_fcla: â\88\80f,L1,L2. â¬\87*[â\93\89, f] L1 â\89\98 L2 →
+                      â\88\83â\88\83n. ð\9d\90\82â¦\83fâ¦\84 â\89\98 n & |L1| = |L2| + n.
 #f #L1 #L2 #H elim H -f -L1 -L2
 [ /4 width=3 by fcla_isid, ex2_intro/
 | #f #I #L1 #L2 #_ * >length_bind /3 width=3 by fcla_next, ex2_intro, eq_f/
@@ -53,53 +53,53 @@ lemma drops_fwd_fcla: ∀f,L1,L2. ⬇*[Ⓣ, f] L1 ≡ L2 →
 qed-.
 
 (* Basic_2A1: includes: drop_fwd_length *)
-lemma drops_fcla_fwd: â\88\80f,L1,L2,n. â¬\87*[â\93\89, f] L1 â\89¡ L2 â\86\92 ð\9d\90\82â¦\83fâ¦\84 â\89¡ n →
+lemma drops_fcla_fwd: â\88\80f,L1,L2,n. â¬\87*[â\93\89, f] L1 â\89\98 L2 â\86\92 ð\9d\90\82â¦\83fâ¦\84 â\89\98 n →
                       |L1| = |L2| + n.
 #f #l1 #l2 #n #Hf #Hn elim (drops_fwd_fcla … Hf) -Hf
 #k #Hm #H <(fcla_mono … Hm … Hn) -f //
 qed-.
 
-lemma drops_fwd_fcla_le2: â\88\80f,L1,L2. â¬\87*[â\93\89, f] L1 â\89¡ L2 →
-                          â\88\83â\88\83n. ð\9d\90\82â¦\83fâ¦\84 â\89¡ n & n ≤ |L1|.
+lemma drops_fwd_fcla_le2: â\88\80f,L1,L2. â¬\87*[â\93\89, f] L1 â\89\98 L2 →
+                          â\88\83â\88\83n. ð\9d\90\82â¦\83fâ¦\84 â\89\98 n & n ≤ |L1|.
 #f #L1 #L2 #H elim (drops_fwd_fcla … H) -H /2 width=3 by ex2_intro/
 qed-.
 
 (* Basic_2A1: includes: drop_fwd_length_le2 *)
-lemma drops_fcla_fwd_le2: â\88\80f,L1,L2,n. â¬\87*[â\93\89, f] L1 â\89¡ L2 â\86\92 ð\9d\90\82â¦\83fâ¦\84 â\89¡ n →
+lemma drops_fcla_fwd_le2: â\88\80f,L1,L2,n. â¬\87*[â\93\89, f] L1 â\89\98 L2 â\86\92 ð\9d\90\82â¦\83fâ¦\84 â\89\98 n →
                           n ≤ |L1|.
 #f #L1 #L2 #n #H #Hn elim (drops_fwd_fcla_le2 … H) -H
 #k #Hm #H <(fcla_mono … Hm … Hn) -f //
 qed-.
 
-lemma drops_fwd_fcla_lt2: â\88\80f,L1,I2,K2. â¬\87*[â\93\89, f] L1 â\89¡ K2.ⓘ{I2} →
-                          â\88\83â\88\83n. ð\9d\90\82â¦\83fâ¦\84 â\89¡ n & n < |L1|.
+lemma drops_fwd_fcla_lt2: â\88\80f,L1,I2,K2. â¬\87*[â\93\89, f] L1 â\89\98 K2.ⓘ{I2} →
+                          â\88\83â\88\83n. ð\9d\90\82â¦\83fâ¦\84 â\89\98 n & n < |L1|.
 #f #L1 #I2 #K2 #H elim (drops_fwd_fcla … H) -H
 #n #Hf #H >H -L1 /3 width=3 by le_S_S, ex2_intro/
 qed-.
 
 (* Basic_2A1: includes: drop_fwd_length_lt2 *)
 lemma drops_fcla_fwd_lt2: ∀f,L1,I2,K2,n.
-                          â¬\87*[â\93\89, f] L1 â\89¡ K2.â\93\98{I2} â\86\92 ð\9d\90\82â¦\83fâ¦\84 â\89¡ n →
+                          â¬\87*[â\93\89, f] L1 â\89\98 K2.â\93\98{I2} â\86\92 ð\9d\90\82â¦\83fâ¦\84 â\89\98 n →
                           n < |L1|.
 #f #L1 #I2 #K2 #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H
 #k #Hm #H <(fcla_mono … Hm … Hn) -f //
 qed-.
 
 (* Basic_2A1: includes: drop_fwd_length_lt4 *)
-lemma drops_fcla_fwd_lt4: â\88\80f,L1,L2,n. â¬\87*[â\93\89, f] L1 â\89¡ L2 â\86\92 ð\9d\90\82â¦\83fâ¦\84 â\89¡ n → 0 < n →
+lemma drops_fcla_fwd_lt4: â\88\80f,L1,L2,n. â¬\87*[â\93\89, f] L1 â\89\98 L2 â\86\92 ð\9d\90\82â¦\83fâ¦\84 â\89\98 n → 0 < n →
                           |L2| < |L1|.
 #f #L1 #L2 #n #H #Hf #Hn lapply (drops_fcla_fwd … H Hf) -f
 /2 width=1 by lt_minus_to_plus_r/ qed-.
 
 (* Basic_2A1: includes: drop_inv_length_eq *)
-lemma drops_inv_length_eq: â\88\80f,L1,L2. â¬\87*[â\93\89, f] L1 â\89¡ L2 → |L1| = |L2| → 𝐈⦃f⦄.
+lemma drops_inv_length_eq: â\88\80f,L1,L2. â¬\87*[â\93\89, f] L1 â\89\98 L2 → |L1| = |L2| → 𝐈⦃f⦄.
 #f #L1 #L2 #H #HL12 elim (drops_fwd_fcla … H) -H
 #n #Hn <HL12 -L2 #H lapply (discr_plus_x_xy … H) -H
 /2 width=3 by fcla_inv_xp/
 qed-.
 
 (* Basic_2A1: includes: drop_fwd_length_eq2 *)
-theorem drops_fwd_length_eq2: â\88\80f,L1,L2,K1,K2. â¬\87*[â\93\89, f] L1 â\89¡ K1 â\86\92 â¬\87*[â\93\89, f] L2 â\89¡ K2 →
+theorem drops_fwd_length_eq2: â\88\80f,L1,L2,K1,K2. â¬\87*[â\93\89, f] L1 â\89\98 K1 â\86\92 â¬\87*[â\93\89, f] L2 â\89\98 K2 →
                               |K1| = |K2| → |L1| = |L2|.
 #f #L1 #L2 #K1 #K2 #HLK1 #HLK2 #HL12
 elim (drops_fwd_fcla … HLK1) -HLK1 #n1 #Hn1 #H1 >H1 -L1
@@ -107,8 +107,8 @@ elim (drops_fwd_fcla … HLK2) -HLK2 #n2 #Hn2 #H2 >H2 -L2
 <(fcla_mono … Hn2 … Hn1) -f //
 qed-.
 
-theorem drops_conf_div: â\88\80f1,f2,L1,L2. â¬\87*[â\93\89, f1] L1 â\89¡ L2 â\86\92 â¬\87*[â\93\89, f2] L1 â\89¡ L2 →
-                        â\88\83â\88\83n. ð\9d\90\82â¦\83f1â¦\84 â\89¡ n & ð\9d\90\82â¦\83f2â¦\84 â\89¡ n.
+theorem drops_conf_div: â\88\80f1,f2,L1,L2. â¬\87*[â\93\89, f1] L1 â\89\98 L2 â\86\92 â¬\87*[â\93\89, f2] L1 â\89\98 L2 →
+                        â\88\83â\88\83n. ð\9d\90\82â¦\83f1â¦\84 â\89\98 n & ð\9d\90\82â¦\83f2â¦\84 â\89\98 n.
 #f1 #f2 #L1 #L2 #H1 #H2
 elim (drops_fwd_fcla … H1) -H1 #n1 #Hf1 #H1
 elim (drops_fwd_fcla … H2) -H2 #n2 #Hf2 >H1 -L1 #H
@@ -116,7 +116,7 @@ lapply (injective_plus_r … H) -L2 #H destruct /2 width=3 by ex2_intro/
 qed-.
 
 theorem drops_conf_div_fcla: ∀f1,f2,L1,L2,n1,n2.
-                             â¬\87*[â\93\89, f1] L1 â\89¡ L2 â\86\92 â¬\87*[â\93\89, f2] L1 â\89¡ L2 â\86\92 ð\9d\90\82â¦\83f1â¦\84 â\89¡ n1 â\86\92 ð\9d\90\82â¦\83f2â¦\84 â\89¡ n2 →
+                             â¬\87*[â\93\89, f1] L1 â\89\98 L2 â\86\92 â¬\87*[â\93\89, f2] L1 â\89\98 L2 â\86\92 ð\9d\90\82â¦\83f1â¦\84 â\89\98 n1 â\86\92 ð\9d\90\82â¦\83f2â¦\84 â\89\98 n2 →
                              n1 = n2.
 #f1 #f2 #L1 #L2 #n1 #n2 #Hf1 #Hf2 #Hn1 #Hn2
 lapply (drops_fcla_fwd … Hf1 Hn1) -f1 #H1