milestone update in ground

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / drops_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma
index dd8ee277c73e20f35ee741c513a5cf386392df0e..ab924e9b8ab483f94109dbf75151dce23b05faa6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma
@@ -88,7 +88,7 @@ qed-.
 (* Basic_2A1: includes: drop_mono *)
 lemma drops_mono: ∀b1,f,L,L1. ⇩*[b1,f] L ≘ L1 →
                   ∀b2,L2. ⇩*[b2,f] L ≘ L2 → L1 = L2.
-#b1 #f #L #L1 lapply (after_isid_dx ð\9d\90\88ð\9d\90\9d … f)
+#b1 #f #L #L1 lapply (after_isid_dx ð\9d\90¢ … f)
 /3 width=8 by drops_conf, drops_fwd_isid/
 qed-.