]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla_uni.ma
update in ground static_2 basic_2 apps_2
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_fcla_uni.ma
index 60fbf8979f2b89e29355d17caf617fd09ab85a1a..d2d7922dfc691a45dea01a2afc850679e2c76c42 100644 (file)
@@ -20,7 +20,7 @@ include "ground/relocation/pr_fcla.ma".
 (* Constructions with pr_uni ************************************************)
 
 (*** fcla_uni *)
-lemma pr_fcla_uni (n): ð\9d\90\82â\9dªð\9d\90®â\9d¨nâ\9d©â\9d« ≘ n.
+lemma pr_fcla_uni (n): ð\9d\90\82â\9d¨ð\9d\90®â\9d¨nâ\9d©â\9d© ≘ n.
 #n @(nat_ind_succ … n) -n
 /2 width=1 by pr_fcla_isi, pr_fcla_next/
 qed.