X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flexs_length.ma;h=3f40c553c4b8e9940ad65cd954b544c3b0550c61;hb=629687db8a55432e95c82f0c79e3f51c023e65a6;hp=c8d3536de1c6c53cabf21c13fc0dbb65cc8c00d7;hpb=5832735b721c0bd8567c8f0be761a9136363a2a6;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma index c8d3536de..3f40c553c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma @@ -15,7 +15,7 @@ include "basic_2/grammar/lenv_length.ma". include "basic_2/relocation/lexs.ma". -(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) +(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) (* Forward lemmas on length for local environments **************************)