update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_fcla_eq.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla_eq.ma
index 0ad95fadd20f526303ee8972a9045dd0ed47e7d6..3675cd9f248947f5e6cea5179c0e342b40025117 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla_eq.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_fcla.ma".
 
 (*** fcla_eq_repl_back *)
 lemma pr_fcla_eq_repl_back (n):
-      pr_eq_repl_back â\80¦ (λf. ð\9d\90\82â\9dªfâ\9d« ≘ n).
+      pr_eq_repl_back â\80¦ (λf. ð\9d\90\82â\9d¨fâ\9d© ≘ n).
 #n #f1 #H elim H -f1 -n /3 width=3 by pr_fcla_isi, pr_isi_eq_repl_back/
 #f1 #n #_ #IH #g2 #H [ elim (pr_eq_inv_push_sn … H) | elim (pr_eq_inv_next_sn … H) ] -H
 /3 width=3 by pr_fcla_push, pr_fcla_next/
@@ -29,6 +29,6 @@ qed-.
 
 (*** fcla_eq_repl_fwd *)
 lemma fcla_eq_repl_fwd (n):
-      pr_eq_repl_fwd â\80¦ (λf. ð\9d\90\82â\9dªfâ\9d« ≘ n).
+      pr_eq_repl_fwd â\80¦ (λf. ð\9d\90\82â\9d¨fâ\9d© ≘ n).
 #n @pr_eq_repl_sym /2 width=3 by pr_fcla_eq_repl_back/
 qed-.