update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / lift_rmap_after.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_after.ma
index e209f97a70e39bdc926135c13fb78e5414e76a52..e3dd359b087a311bc2ebbe8684754bcd97e3b3e6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_after.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_after.ma
@@ -20,7 +20,7 @@ include "delayed_updating/substitution/lift_path.ma".
 (* Constructions with tr_after **********************************************)
 
 lemma lift_rmap_after (g) (f) (p:path):
-      ↑[↑[f]p]g∘↑[p]f = ↑[p](g∘f).
+      🠢[g]🠡[f]p∘🠢[f]p = 🠢[g∘f]p.
 #g #f #p elim p -p //
 #l #p #IH
 <lift_rmap_rcons //