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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap.ma
index dcec9b57a..94c358d1b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/notation/functions/uparrow_2.ma".
+include "delayed_updating/notation/functions/righttrianglearrow_2.ma".
 include "delayed_updating/syntax/label.ma".
 include "ground/relocation/tr_pn.ma".
 include "ground/lib/stream_tls.ma".
@@ -30,26 +30,26 @@ match l with
 
 interpretation
   "prelift (relocation map)"
-  'UpArrow l f = (prelift_rmap f l).
+  'RightTriangleArrow f l = (prelift_rmap f l).
 
 (* Basic constructions ******************************************************)
 
 lemma prelift_rmap_d (f) (k:pnat):
-      ⇂*[k]f = ↑[𝗱k]f.
+      ⇂*[k]f = 🠢[f]𝗱k.
 // qed.
 
 lemma prelift_rmap_m (f):
-      f = ↑[𝗺]f.
+      f = 🠢[f]𝗺.
 // qed.
 
 lemma prelift_rmap_L (f):
-      (⫯f) = ↑[𝗟]f.
+      (⫯f) = 🠢[f]𝗟.
 // qed.
 
 lemma prelift_rmap_A (f):
-      f = ↑[𝗔]f.
+      f = 🠢[f]𝗔.
 // qed.
 
 lemma prelift_rmap_S (f):
-      f = ↑[𝗦]f.
+      f = 🠢[f]𝗦.
 // qed.