X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fgr_isu_tl.ma;h=8a7b07df1792ffe56c6f8901acbb3dc9f7c17228;hb=dc605ae41c39773f55381f241b1ed3db4acf5edd;hp=73fa585b7086ddfc8ce21d3b57a3ec41c6d0c695;hpb=caf822cbe34e204e6d1b72e272373b561c1a565a;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_tl.ma index 73fa585b7..8a7b07df1 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_tl.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_tl.ma @@ -19,7 +19,7 @@ include "ground/relocation/gr_isu.ma". (* Constructions with gr_tl *************************************************) -lemma gr_isu_tl (f): 𝐔❪f❫ → 𝐔❪⫱f❫. +lemma gr_isu_tl (f): 𝐔❪f❫ → 𝐔❪⫰f❫. #f cases (gr_map_split_tl f) * #H [ /3 width=3 by gr_isu_inv_push, gr_isu_isi/ | /2 width=3 by gr_isu_inv_next/