renaming in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / fsle_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fsle_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fsle_drops.ma
index 7ca1aa2147144b326cf614c8b9b3e7a3c57021a2..441c6b468df6ca86817de617fcbf9ad63ad468c7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/fsle_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/fsle_drops.ma
@@ -19,7 +19,7 @@ include "basic_2/static/fsle_length.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma fsle_lifts_sn: â\88\80T1,U1. â¬\86*[1] T1 â\89¡ U1 → ∀L1,L2. |L2| ≤ |L1| →
+lemma fsle_lifts_sn: â\88\80T1,U1. â¬\86*[1] T1 â\89\98 U1 → ∀L1,L2. |L2| ≤ |L1| →
                      ∀T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ → ⦃L1.ⓧ, U1⦄ ⊆ ⦃L2, T2⦄.
 #T1 #U1 #HTU1 #L1 #L2 #H1L #T2
 * #n #m #f #g #Hf #Hg #H2L #Hfg
@@ -30,7 +30,7 @@ lapply (frees_lifts_SO (Ⓣ) (L1.ⓧ) … HTU1 … Hf)
 qed-.
 
 lemma fsle_lifts_SO_sn: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1, V1⦄ ⊆ ⦃K2, V2⦄ →
-                        â\88\80W1. â¬\86*[1] V1 â\89¡ W1 → ∀I1,I2. ⦃K1.ⓘ{I1}, W1⦄ ⊆ ⦃K2.ⓑ{I2}V2, #O⦄.
+                        â\88\80W1. â¬\86*[1] V1 â\89\98 W1 → ∀I1,I2. ⦃K1.ⓘ{I1}, W1⦄ ⊆ ⦃K2.ⓑ{I2}V2, #O⦄.
 #K1 #K2 #HK #V1 #V2
 * #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12
 #W1 #HVW1 #I1 #I2
@@ -39,7 +39,7 @@ elim (lveq_inj_length … HK12) // -HK #H1 #H2 destruct
 qed.
 
 lemma fsle_lifts_SO: ∀K1,K2. |K1| = |K2| → ∀T1,T2. ⦃K1, T1⦄ ⊆ ⦃K2, T2⦄ →
-                     â\88\80U1,U2. â¬\86*[1] T1 â\89¡ U1 â\86\92 â¬\86*[1] T2 â\89¡ U2 →
+                     â\88\80U1,U2. â¬\86*[1] T1 â\89\98 U1 â\86\92 â¬\86*[1] T2 â\89\98 U2 →
                      ∀I1,I2.  ⦃K1.ⓘ{I1}, U1⦄ ⊆ ⦃K2.ⓘ{I2}, U2⦄.
 #K1 #K2 #HK #T1 #T2
 * #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12
@@ -50,7 +50,7 @@ qed.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma fsle_inv_lifts_sn: â\88\80T1,U1. â¬\86*[1] T1 â\89¡ U1 →
+lemma fsle_inv_lifts_sn: â\88\80T1,U1. â¬\86*[1] T1 â\89\98 U1 →
                          ∀I1,I2,L1,L2,V1,V2,U2. ⦃L1.ⓑ{I1}V1,U1⦄ ⊆ ⦃L2.ⓑ{I2}V2, U2⦄ →
                          ∀p. ⦃L1, T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.U2⦄.
 #T1 #U1 #HTU1 #I1 #I2 #L1 #L2 #V1 #V2 #U2