update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap_after.ma
index 3e83fbbf8de3eeddf3a4cb0905c10df806679307..edb2ae01d3fa0ccd7b59e14c036f33aa68971f12 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap_after.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap_after.ma
@@ -22,7 +22,7 @@ include "ground/relocation/tr_compose_tls.ma".
 (* Constructions with tr_after **********************************************)
 
 lemma prelift_rmap_after (g) (f) (l):
-      ↑[↑[f]l]g∘↑[l]f = ↑[l](g∘f).
+      🠢[g]🠡[f]l∘🠢[f]l = 🠢[g∘f]l.
 #g #f * [ #k ] //
 <prelift_rmap_d //
 qed.