update in ground, static_2 and apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma
index 94592fdfdbc0ac323c4fe957dac035f66ba5078c..43b69b3f0395a04a160e39ff7e8777468d2b81d3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma
@@ -29,9 +29,9 @@ corec theorem pr_eq_trans: Transitive … pr_eq.
 qed-.
 
 (*** eq_canc_sn *)
-theorem pr_eq_canc_sn (f2): pr_eq_repl_back (λf. f â\89¡ f2).
+theorem pr_eq_canc_sn (f2): pr_eq_repl_back (λf. f â\89\90 f2).
 /3 width=3 by pr_eq_trans, pr_eq_sym/ qed-.
 
 (*** eq_canc_dx *)
-theorem pr_eq_canc_dx (f1): pr_eq_repl_fwd (λf. f1 â\89¡ f).
+theorem pr_eq_canc_dx (f1): pr_eq_repl_fwd (λf. f1 â\89\90 f).
 /3 width=5 by pr_eq_canc_sn, pr_eq_repl_sym/ qed-.