]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla_fcla.ma
update in ground static_2 basic_2 apps_2
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_fcla_fcla.ma
index 8aa59f952e7428a5fb2b6aa10207e7cfd05a7a96..0c3481a2156217aac305945f54d3068eb286e6fa 100644 (file)
@@ -20,7 +20,7 @@ include "ground/relocation/pr_fcla.ma".
 
 (*** fcla_mono *)
 theorem pr_fcla_mono (f):
-        â\88\80n1. ð\9d\90\82â\9dªfâ\9d« â\89\98 n1 â\86\92 â\88\80n2. ð\9d\90\82â\9dªfâ\9d« ≘ n2 → n1 = n2.
+        â\88\80n1. ð\9d\90\82â\9d¨fâ\9d© â\89\98 n1 â\86\92 â\88\80n2. ð\9d\90\82â\9d¨fâ\9d© ≘ n2 → n1 = n2.
 #f #n #H elim H -f -n
 [ /2 width=3 by pr_fcla_inv_isi/
 | /3 width=3 by pr_fcla_inv_push/