partial commit in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / seq.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma
index 128cd29749b7cf46787ae7fb6dbf5da5665d9909..224102f015f761e0547d4d074742d2518495dba7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma
@@ -19,7 +19,7 @@ include "static_2/relocation/sex.ma".
 (* SYNTACTIC EQUIVALENCE FOR SELECTED LOCAL ENVIRONMENTS ********************)
 
 (* Basic_2A1: includes: lreq_atom lreq_zero lreq_pair lreq_succ *)
-definition seq: relation3 rtmap lenv lenv ≝
+definition seq: relation3 pr_map lenv lenv ≝
            sex ceq_ext cfull.
 
 interpretation
@@ -29,11 +29,11 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma seq_eq_repl_back:
-      ∀L1,L2. eq_repl_back … (λf. L1 ≡[f] L2).
+      ∀L1,L2. pr_eq_repl_back … (λf. L1 ≡[f] L2).
 /2 width=3 by sex_eq_repl_back/ qed-.
 
 lemma seq_eq_repl_fwd:
-      ∀L1,L2. eq_repl_fwd … (λf. L1 ≡[f] L2).
+      ∀L1,L2. pr_eq_repl_fwd … (λf. L1 ≡[f] L2).
 /2 width=3 by sex_eq_repl_fwd/ qed-.
 
 lemma sle_seq_trans: