X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ffr2_nat_nat.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ffr2_nat_nat.ma;h=744becdada3f64dbfd45d87b0e602dcd1599e8d1;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=a40ac35c15e8e3e322cd7cafb5d0d22e7510fd3c;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
index a40ac35c1..744becdad 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
@@ -20,7 +20,7 @@ include "ground/relocation/fr2_nat.ma".
 
 (*** at_mono *)
 theorem fr2_nat_mono (f) (l):
-        ∀l1. @❪l, f❫ ≘ l1 → ∀l2. @❪l, f❫ ≘ l2 → l1 = l2.
+        ∀l1. @❨l, f❩ ≘ l1 → ∀l2. @❨l, f❩ ≘ l2 → l1 = l2.
 #f #l #l1 #H elim H -f -l -l1
 [ #l #x #H <(fr2_nat_inv_nil … H) -x //
 | #f #d #h #l #l1 #Hld #_ #IH #x #H