]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma
advances in the theory of drops, lexs, and frees ...
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / lexs_length.ma
index c8d3536de1c6c53cabf21c13fc0dbb65cc8c00d7..3f40c553c4b8e9940ad65cd954b544c3b0550c61 100644 (file)
@@ -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 **************************)