X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_isd_tl.ma;h=7406b90afcbf066a964f1ac072b8e95535c85404;hb=df1bcd1387439133c0c33f597a5f8b2331c07772;hp=50f83a41ccb95e88c74e4b0cf00479729662b419;hpb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_tl.ma
index 50f83a41c..7406b90af 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_tl.ma
@@ -20,7 +20,7 @@ include "ground/relocation/pr_isd.ma".
 (* Constructions with pr_tl *************************************************)
 
 (*** isdiv_tl *)
-lemma pr_isd_tl (f): 𝛀❪f❫ → 𝛀❪⫰f❫.
+lemma pr_isd_tl (f): 𝛀❨f❩ → 𝛀❨⫰f❩.
 #f cases (pr_map_split_tl f) * #H
 [ elim (pr_isd_inv_push … H) -H //
 | /2 width=3 by pr_isd_inv_next/