X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flex.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flex.ma;h=240c00d608e47f7c7cdf1cfbd9e6a8a9785fbbe0;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=02ba4bedc837ea1318c83fb27239cb9456ca0f35;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma
index 02ba4bedc..240c00d60 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma
@@ -21,7 +21,7 @@ include "static_2/relocation/sex.ma".
 (* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **************)
 
 definition lex (R): relation lenv ≝
-                    λL1,L2. ∃∃f. 𝐈❪f❫ & L1 ⪤[cfull,cext2 R,f] L2.
+                    λL1,L2. ∃∃f. 𝐈❨f❩ & L1 ⪤[cfull,cext2 R,f] L2.
 
 interpretation "generic extension (local environment)"
    'Relation R L1 L2 = (lex R L1 L2).