update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma
index 5af9e1664a4cd60d7b6b24b6ea475a2d10ac0d3b..140dd6f8ac6ec113df5c51562b258fc38f434292 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma
@@ -21,7 +21,7 @@ include "delayed_updating/substitution/lift_path_structure.ma".
 (* Constructions with lift_path *********************************************)
 
 lemma lift_unwind2_path_after (g) (f) (p):
-      ↑[g]▼[f]p = ▼[g∘f]p.
+      🠡[g]▼[f]p = ▼[g∘f]p.
 #g #f * // * [ #k ] #p //
 <unwind2_path_d_dx <unwind2_path_d_dx <lift_path_d_dx
 <lift_path_structure >tr_compose_pap
@@ -29,7 +29,7 @@ lemma lift_unwind2_path_after (g) (f) (p):
 qed.
 
 lemma unwind2_lift_path_after (g) (f) (p):
-      ▼[g]↑[f]p = ▼[g∘f]p.
+      ▼[g]🠡[f]p = ▼[g∘f]p.
 #g #f * // * [ #k ] #p
 [ <unwind2_path_d_dx <unwind2_path_d_dx
   <structure_lift_path >tr_compose_pap