update in delayed_updating

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

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 c23c1a0a6f32d6b41b51b7eb411e29a0de406fe9..5089e60ea04b53a7af7eebb982b7363c0441ccc5 100644 (file)
--- 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.