update in delayed_updating

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

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 02c51eca2b0d2db805f05f77b76506c0ca75ee8d..b42274ef822c82248534dbcd6e3c7546d323b6e2 100644 (file)
--- 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 …))