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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_lift.ma
index 02c51eca2..b42274ef8 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_lift.ma
@@ -23,7 +23,7 @@ include "delayed_updating/syntax/path_structure.ma".
 (* Constructions with lift_path *********************************************)
 
 lemma lift_unwind2_rmap_after (g) (f) (p):
-      ↑[⊗p]g∘▶[f]p ≗ ▶[g∘f]p.
+      🠢[g]⊗p∘▶[f]p ≗ ▶[g∘f]p.
 #g #f #p elim p -p //
 * [ #k ] #p #IH //
 [ <unwind2_rmap_d_dx <unwind2_rmap_d_dx
@@ -35,7 +35,7 @@ lemma lift_unwind2_rmap_after (g) (f) (p):
 qed.
 
 lemma unwind2_lift_rmap_after (g) (f) (p:path):
-      ▶[g]↑[f]p∘↑[p]f ≗ ▶[g∘f]p.
+      ▶[g]🠡[f]p∘🠢[f]p ≗ ▶[g∘f]p.
 #g #f #p elim p -p // #l #p #IH
 <lift_path_rcons <lift_rmap_rcons <unwind2_rmap_rcons <unwind2_rmap_rcons
 @(stream_eq_trans … (preunwind2_lift_rmap_after …))