X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_rmap_eq.ma;h=790b2e6054c0734ff88c98484494ce4301154b7a;hp=bf5151f00a852df4b855705ad94817cea27b2e88;hb=7008128d354c6e998a87bc2febe9f86ea714869c;hpb=d06053844638d88936d711b66fddbcca2a9add1c

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma
index bf5151f00..790b2e605 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma
@@ -23,14 +23,14 @@ include "ground/arith/nat_rplus_pplus.ma".
 (* Constructions with lift_eq ***********************************************)
 
 lemma lift_rmap_eq_repl (p):
-      stream_eq_repl … (λf1,f2. ↑[p]f1 ≗ ↑[p]f2).
+      stream_eq_repl … (λf1,f2. 🠢[f1]p ≗ 🠢[f2]p).
 #p elim p -p //
 #l #p #IH #f1 #f2 #Hf
 /3 width=1 by prelift_rmap_eq_repl/
 qed.
 
 lemma tls_lift_rmap_d_dx (f) (p) (n) (k):
-      ⇂*[n+k]↑[p]f ≗ ⇂*[n]↑[p◖𝗱k]f.
+      ⇂*[n+k]🠢[f]p ≗ ⇂*[n]🠢[f](p◖𝗱k).
 #f #p #n #k
 <lift_rmap_d_dx >nrplus_inj_dx >nrplus_inj_sn //
 qed.