X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flexs_lexs.ma;h=a22e62c86140da816cc520ec8b2eef9c3b0fc085;hb=629687db8a55432e95c82f0c79e3f51c023e65a6;hp=1b8aa44cb63d1e6533821f9452a671676757d976;hpb=5832735b721c0bd8567c8f0be761a9136363a2a6;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma index 1b8aa44cb..a22e62c86 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma @@ -17,7 +17,7 @@ include "ground_2/relocation/rtmap_sor.ma". include "basic_2/grammar/lenv_weight.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 *****) (* Main properties **********************************************************) @@ -58,7 +58,7 @@ theorem lexs_conf: ∀RN1,RP1,RN2,RP2. ] qed-. -theorem lexs_canc_sx: ∀RN,RP,f. Transitive … (lexs RN RP f) → +theorem lexs_canc_sn: ∀RN,RP,f. Transitive … (lexs RN RP f) → symmetric … (lexs RN RP f) → left_cancellable … (lexs RN RP f). /3 width=3 by/ qed-.