]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma
update in ground static_2 basic_2 apps_2
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / lex.ma
index 02ba4bedc837ea1318c83fb27239cb9456ca0f35..240c00d608e47f7c7cdf1cfbd9e6a8a9785fbbe0 100644 (file)
@@ -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. â\88\83â\88\83f. ð\9d\90\88â\9dªfâ\9d« & L1 ⪤[cfull,cext2 R,f] L2.
+                    Î»L1,L2. â\88\83â\88\83f. ð\9d\90\88â\9d¨fâ\9d© & L1 ⪤[cfull,cext2 R,f] L2.
 
 interpretation "generic extension (local environment)"
    'Relation R L1 L2 = (lex R L1 L2).