X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Fprelift_rmap_eq.ma;h=5089e60ea04b53a7af7eebb982b7363c0441ccc5;hb=7008128d354c6e998a87bc2febe9f86ea714869c;hp=c23c1a0a6f32d6b41b51b7eb411e29a0de406fe9;hpb=5c2d38b46908f662cbb717156b29101ff30f8352;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap_eq.ma
index c23c1a0a6..5089e60ea 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap_eq.ma
@@ -21,6 +21,6 @@ include "ground/lib/stream_tls_eq.ma".
 (* constructions with tr_map_eq *********************************************)
 
 lemma prelift_rmap_eq_repl (l):
-      stream_eq_repl … (λf1,f2. ↑[l]f1 ≗ ↑[l]f2).
+      stream_eq_repl … (λf1,f2. 🠢[f1]l ≗ 🠢[f2]l).
 * //
 qed.