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

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.