X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fgr_isu_tl.ma;h=8a7b07df1792ffe56c6f8901acbb3dc9f7c17228;hb=8bbe582d87984526f40182c4409cbfd43108cb79;hp=73fa585b7086ddfc8ce21d3b57a3ec41c6d0c695;hpb=2ed8d2abcc3b0687141b627061b63350a0b200bd;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/