X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fmultiple%2Fdrops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fmultiple%2Fdrops.ma;h=87f93c4f92941550c419de56b4f5cfacfe5841b8;hb=291fe1d3b56faf91d07099f43f3ebde2988649e1;hp=cd7fc2211142ec83b90a283ecc5e004a226b2c33;hpb=b5507c449ba38a76666a35664f9cf4e1953ad8ec;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops.ma
index cd7fc2211..87f93c4f9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops.ma
@@ -24,7 +24,7 @@ include "basic_2A/multiple/lifts_vector.ma".
 inductive drops (s:bool): mr2 → relation lenv ≝
 | drops_nil : ∀L. drops s (𝐞) L L
 | drops_cons: ∀L1,L,L2,cs,l,m.
-              drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s (❨l, m❩; cs) L1 L2
+              drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s (❨l, m❩◗ cs) L1 L2
 .
 
 interpretation "iterated slicing (local environment) abstract"
@@ -58,7 +58,7 @@ lemma drops_inv_nil: ∀L1,L2,s. ⬇*[s, 𝐞] L1 ≡ L2 → L1 = L2.
 /2 width=4 by drops_inv_nil_aux/ qed-.
 
 fact drops_inv_cons_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 →
-                         ∀l,m,tl. cs = ❨l, m❩; tl →
+                         ∀l,m,tl. cs = ❨l, m❩◗ tl →
                          ∃∃L. ⬇*[s, tl] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
 #L1 #L2 #s #cs * -L1 -L2 -cs
 [ #L #l #m #tl #H destruct
@@ -67,7 +67,7 @@ fact drops_inv_cons_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 →
 ]
 qed-.
 
-lemma drops_inv_cons: ∀L1,L2,s,l,m,cs. ⬇*[s, ❨l, m❩; cs] L1 ≡ L2 →
+lemma drops_inv_cons: ∀L1,L2,s,l,m,cs. ⬇*[s, ❨l, m❩◗ cs] L1 ≡ L2 →
                       ∃∃L. ⬇*[s, cs] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
 /2 width=3 by drops_inv_cons_aux/ qed-.