X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Fprelift_rmap_after.ma;h=edb2ae01d3fa0ccd7b59e14c036f33aa68971f12;hp=3e83fbbf8de3eeddf3a4cb0905c10df806679307;hb=7008128d354c6e998a87bc2febe9f86ea714869c;hpb=d06053844638d88936d711b66fddbcca2a9add1c

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 3e83fbbf8..edb2ae01d 100644
--- 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.