partial commit in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / path_labels.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma
index e7e1391da6313ed92d874bad2ec09bdce551870e..7f0a71a8c34b323005c19924048d6f90e7de4905 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma
@@ -36,7 +36,7 @@ lemma labels_zero (l):
 // qed.
 
 lemma labels_succ (l) (n):
-      l◗(l∗∗n) = l∗∗(↑n).
+      (l∗∗n)◖l = l∗∗(↑n).
 #l #n
 <labels_unfold <labels_unfold <niter_succ //
 qed.