update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / unwind / preunwind2_rmap_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_lift.ma
index f5317dbf3964da57936f6474534b3d6db7340512..cc5b351ad71faca3183f97a272d5397c796aef3d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_lift.ma
@@ -25,7 +25,7 @@ include "ground/lib/stream_eq_eq.ma".
 (* Constructions with lift_path *********************************************)
 
 lemma preunwind2_lift_rmap_after (g) (f) (l):
-      ▶[g]↑[f]l∘↑[l]f ≗ ▶[g∘f]l.
+      ▶[g]🠡[f]l∘🠢[f]l ≗ ▶[g∘f]l.
 #g #f * // #k
 <prelift_label_d <prelift_rmap_d <preunwind2_rmap_d <preunwind2_rmap_d
 @(stream_eq_trans … (tr_compose_assoc …))