X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fseq.ma;h=224102f015f761e0547d4d074742d2518495dba7;hp=128cd29749b7cf46787ae7fb6dbf5da5665d9909;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hpb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma
index 128cd2974..224102f01 100644
--- 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: