X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flexs.ma;h=9587c2659096f70d55dffa66440463219951e36a;hb=045c74915022181e288d9a950cc485437b08d002;hp=d0dbc756838768eaac6d596985ab1b287ad7dee3;hpb=4b1dee70d9f24b47ab1f93cf1e63862b7b71a645;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 d0dbc7568..9587c2659 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
@@ -32,7 +32,7 @@ inductive lexs (RN,RP:relation3 lenv term term): rtmap → relation lenv ≝
 interpretation "generic entrywise extension (local environment)"
    'RelationStar RN RP f L1 L2 = (lexs RN RP f L1 L2).
 
-definition lexs_pw_confluent2_R: relation3 lenv term term → relation3 lenv term term →
+definition R_pw_confluent2_lexs: relation3 lenv term term → relation3 lenv term term →
                                  relation3 lenv term term → relation3 lenv term term →
                                  relation3 lenv term term → relation3 lenv term term →
                                  relation3 rtmap lenv term ≝