update in basic_2 and ground_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_isfin.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
index 875378b987c00d56b339ed8ffeb79163b6a15165..29f6eca5a79212539437b59770c5fdd265a59cbc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
@@ -18,7 +18,7 @@ include "ground_2/relocation/rtmap_fcla.ma".
 (* RELOCATION MAP ***********************************************************)
 
 definition isfin: predicate rtmap ≝
-                  λf. â\88\83n. ð\9d\90\82â¦\83fâ¦\84 â\89¡ n.
+                  λf. â\88\83n. ð\9d\90\82â¦\83fâ¦\84 â\89\98 n.
 
 interpretation "test for finite colength (rtmap)"
    'IsFinite f = (isfin f).