update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label_after.ma
index 24720288b107923ac973a635d187dc51ec468e87..f43f1b647dcae9e90c756514e330ea5374c1df0a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label_after.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label_after.ma
@@ -20,6 +20,6 @@ include "ground/relocation/tr_compose_pap.ma".
 (* Constructions with tr_after **********************************************)
 
 lemma prelift_label_after (g) (f) (l):
-      ↑[g]↑[f]l = ↑[g∘f]l.
+      🠡[g]🠡[f]l = 🠡[g∘f]l.
 #g #f * [ #k ] //
 qed.