X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flexs.ma;h=8140a5d31091fcb23900b7c69d3a5c8929f9d591;hb=629687db8a55432e95c82f0c79e3f51c023e65a6;hp=d89370b417b0b084e28e6094223623921dd46b1b;hpb=5832735b721c0bd8567c8f0be761a9136363a2a6;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index d89370b41..8140a5d31 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -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 A CONTEXT-SENSITIVE REALTION FOR TERMS ****) +(* GENERAL 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.