update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / prelift_rmap.ma

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 de7f40321f9052b9c11878eb7b3ef8177323699d..94c358d1ba248d7bf1a2ed739f770495db79d3d7 100644 (file)
--- 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".
@@ -21,7 +21,7 @@ include "ground/lib/stream_tls.ma".
 
 definition prelift_rmap (f) (l): tr_map ≝
 match l with
-[ label_d n ⇒ ⇂*[n]f
+[ label_d k ⇒ ⇂*[k]f
 | label_m   ⇒ f
 | label_L   ⇒ ⫯f
 | label_A   ⇒ f
@@ -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) (n:pnat):
-      ⇂*[n]f = ↑[𝗱n]f.
+lemma prelift_rmap_d (f) (k:pnat):
+      ⇂*[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.