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

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 f5317dbf3..cc5b351ad 100644
--- 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 …))