X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_isfin.ma;h=29f6eca5a79212539437b59770c5fdd265a59cbc;hb=75f395f0febd02de8e0f881d918a8812b1425c8d;hp=875378b987c00d56b339ed8ffeb79163b6a15165;hpb=d59f344b1e4b377e2f06abd9f8856d686d21b222;p=helm.git

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 875378b98..29f6eca5a 100644
--- 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. ∃n. 𝐂⦃f⦄ ≡ n.
+                  λf. ∃n. 𝐂⦃f⦄ ≘ n.
 
 interpretation "test for finite colength (rtmap)"
    'IsFinite f = (isfin f).