update in ground, static_2 and apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma
index 610ba9c7dce081cfe1a00ed2df5e22205d863d81..c908a6ac3f20c376f31be3f208ffd3ec109e8482 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ground/xoa/ex_3_2.ma".
-include "ground/notation/relations/ideq_2.ma".
+include "ground/notation/relations/doteq_2.ma".
 include "ground/lib/stream_eq.ma".
 include "ground/relocation/pr_map.ma".
 
@@ -31,19 +31,19 @@ coinductive pr_eq: relation pr_map ≝
 
 interpretation
   "extensional equivalence (partial relocation maps)"
-  'IdEq f1 f2 = (pr_eq f1 f2).
+  'DotEq f1 f2 = (pr_eq f1 f2).
 
 (*** eq_repl *)
 definition pr_eq_repl (R:relation …) ≝
-           â\88\80f1,f2. f1 â\89¡ f2 → R f1 f2.
+           â\88\80f1,f2. f1 â\89\90 f2 → R f1 f2.
 
 (*** eq_repl_back *)
 definition pr_eq_repl_back (R:predicate …) ≝
-           â\88\80f1. R f1 â\86\92 â\88\80f2. f1 â\89¡ f2 → R f2.
+           â\88\80f1. R f1 â\86\92 â\88\80f2. f1 â\89\90 f2 → R f2.
 
 (*** eq_repl_fwd *)
 definition pr_eq_repl_fwd (R:predicate …) ≝
-           â\88\80f1. R f1 â\86\92 â\88\80f2. f2 â\89¡ f1 → R f2.
+           â\88\80f1. R f1 â\86\92 â\88\80f2. f2 â\89\90 f1 → R f2.
 
 (* Basic constructions ******************************************************)