X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fgr_ist.ma;h=d7f511a56fa1ef8c75a71b1125ab9725f7033756;hp=8a3636574798a7a9ce6ce3a64612fbb8365aca5d;hb=dc605ae41c39773f55381f241b1ed3db4acf5edd;hpb=caf822cbe34e204e6d1b72e272373b561c1a565a

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist.ma
index 8a3636574..d7f511a56 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist.ma
@@ -42,7 +42,7 @@ qed-.
 (* Constructions with gr_tl *************************************************)
 
 (*** istot_tl *)
-lemma gr_ist_tl (f): 𝐓❪f❫ → 𝐓❪⫱f❫.
+lemma gr_ist_tl (f): 𝐓❪f❫ → 𝐓❪⫰f❫.
 #f cases (gr_map_split_tl f) *
 /2 width=3 by gr_ist_inv_next, gr_ist_inv_push/
 qed.