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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla_uni.ma
index 60fbf8979..d2d7922df 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla_uni.ma
@@ -20,7 +20,7 @@ include "ground/relocation/pr_fcla.ma".
 (* Constructions with pr_uni ************************************************)
 
 (*** fcla_uni *)
-lemma pr_fcla_uni (n): 𝐂❪𝐮❨n❩❫ ≘ n.
+lemma pr_fcla_uni (n): 𝐂❨𝐮❨n❩❩ ≘ n.
 #n @(nat_ind_succ … n) -n
 /2 width=1 by pr_fcla_isi, pr_fcla_next/
 qed.