notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / cpys.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma
index c7d59d176b905b282e1ba69a00ed1c53585af5b7..eda8ee1e14a87513af7465b2aab1fad673e13c2b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma
@@ -98,9 +98,9 @@ qed-.
 (* Basic forward lemmas *****************************************************)
 
 lemma cpys_fwd_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
-                   â\88\80T1,d,e. â\87§[d, e] T1 ≡ U1 →
+                   â\88\80T1,d,e. â¬\86[d, e] T1 ≡ U1 →
                    d ≤ dt → d + e ≤ dt + et →
-                   â\88\83â\88\83T2. â¦\83G, Lâ¦\84 â\8a¢ U1 â\96¶*[d+e, dt+et-(d+e)] U2 & â\87§[d, e] T2 ≡ U2.
+                   â\88\83â\88\83T2. â¦\83G, Lâ¦\84 â\8a¢ U1 â\96¶*[d+e, dt+et-(d+e)] U2 & â¬\86[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H #T1 #d #e #HTU1 #Hddt #Hdedet @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HU1 #HTU
@@ -160,7 +160,7 @@ lemma cpys_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶*[d, 0] T2 → T1 =
 qed-.
 
 lemma cpys_inv_lift1_eq: ∀G,L,U1,U2. ∀d,e:nat.
-                         â¦\83G, Lâ¦\84 â\8a¢ U1 â\96¶*[d, e] U2 â\86\92 â\88\80T1. â\87§[d, e] T1 ≡ U1 → U1 = U2.
+                         â¦\83G, Lâ¦\84 â\8a¢ U1 â\96¶*[d, e] U2 â\86\92 â\88\80T1. â¬\86[d, e] T1 ≡ U1 → U1 = U2.
 #G #L #U1 #U2 #d #e #H #T1 #HTU1 @(cpys_ind … H) -U2
 /2 width=7 by cpy_inv_lift1_eq/
 qed-.