]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
- minor corrections
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / lexs.ma
index a79a3e4d9a3559d2077584c65778844da9aa1d77..753a62bc5fd1f1585cd38afacb2fcee42b117572 100644 (file)
@@ -16,7 +16,7 @@ include "ground_2/relocation/rtmap_sle.ma".
 include "basic_2/notation/relations/relationstar_5.ma".
 include "basic_2/grammar/lenv.ma".
 
-(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
+(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
 
 definition relation5 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0]
 ≝ λA,B,C,D,E.A→B→C→D→E→Prop.