X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fgr_tls_pushs.ma;h=1bc1578d7b8f50458ee5a58323b7c3aac16e7799;hb=8bbe582d87984526f40182c4409cbfd43108cb79;hp=7eb749d1b90e887d8edbc2c5ee7c741a4724ea06;hpb=55c768d7e45babb300b5010463ba3196a68f1bbe;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs.ma index 7eb749d1b..1bc1578d7 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs.ma @@ -15,12 +15,12 @@ include "ground/relocation/gr_pushs.ma". include "ground/relocation/gr_tls.ma". -(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************) +(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************) -(* Properties with pushs ****************************************************) +(* Constructions with gr_pushs **********************************************) (*** tls_pushs *) -lemma gr_tls_pushs (n) (f): f = ⫱*[n] ⫯*[n] f. +lemma gr_tls_pushs (n) (f): f = ⫰*[n] ⫯*[n] f. #n @(nat_ind_succ … n) -n // #n #IH #f