X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_tl_eq_eq.ma;h=43b69b3f0395a04a160e39ff7e8777468d2b81d3;hb=873fb39bdd21aa14877bf5d50db26e3a050c6d43;hp=94592fdfdbc0ac323c4fe957dac035f66ba5078c;hpb=503500ff9a6d9cca363a42b5fe7f3f5de69239f9;p=helm.git

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 94592fdfd..43b69b3f0 100644
--- 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 ≡ f2).
+theorem pr_eq_canc_sn (f2): pr_eq_repl_back (λf. f ≐ 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 ≡ f).
+theorem pr_eq_canc_dx (f1): pr_eq_repl_fwd (λf. f1 ≐ f).
 /3 width=5 by pr_eq_canc_sn, pr_eq_repl_sym/ qed-.