X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flex.ma;h=76381a9faba10bdac541bd41d8395db1d991d360;hp=1900d273dd0010bfb8da8ecf6eed4d2c1629542f;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma
index 1900d273d..76381a9fa 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma
@@ -22,7 +22,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).