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

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 5af9e1664..140dd6f8a 100644
--- 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