X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Fdrops_drop.ma;h=99b69bdc714f9eb8b47598bbc3033d9ba7b9315d;hb=43282d3750af8831c8100c60d75c56fdfb7ff3c9;hp=20722888785869aac6fced23bda95fb3e6fe9a18;hpb=6c985e4e2e7846a2b9abd0c84569f21c24e9ce2f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drop.ma
index 207228887..99b69bdc7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drop.ma
@@ -19,8 +19,8 @@ include "basic_2/multiple/drops.ma".
 
 (* Properties concerning basic local environment slicing ********************)
 
-lemma drops_drop_trans: ∀L1,L,des. ⇩*[Ⓕ, des] L1 ≡ L → ∀L2,i. ⇩[i] L ≡ L2 →
-                        ∃∃L0,des0,i0. ⇩[i0] L1 ≡ L0 & ⇩*[Ⓕ, des0] L0 ≡ L2 &
+lemma drops_drop_trans: ∀L1,L,des. ⬇*[Ⓕ, des] L1 ≡ L → ∀L2,i. ⬇[i] L ≡ L2 →
+                        ∃∃L0,des0,i0. ⬇[i0] L1 ≡ L0 & ⬇*[Ⓕ, des0] L0 ≡ L2 &
                                       @⦃i, des⦄ ≡ i0 & des ▭ i ≡ des0.
 #L1 #L #des #H elim H -L1 -L -des
 [ /2 width=7 by drops_nil, minuss_nil, at_nil, ex4_3_intro/