X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fdrops_drops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fdrops_drops.ma;h=ab924e9b8ab483f94109dbf75151dce23b05faa6;hb=55c768d7e45babb300b5010463ba3196a68f1bbe;hp=dd8ee277c73e20f35ee741c513a5cf386392df0e;hpb=15212e44902f25536f6e2de4bec4cedcd9a9804d;p=helm.git

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 dd8ee277c..ab924e9b8 100644
--- 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 𝐈𝐝 … f)
+#b1 #f #L #L1 lapply (after_isid_dx 𝐢 … f)
 /3 width=8 by drops_conf, drops_fwd_isid/
 qed-.