X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_labels.ma;h=7f0a71a8c34b323005c19924048d6f90e7de4905;hb=df1bcd1387439133c0c33f597a5f8b2331c07772;hp=a01c225ee50b1c9575bb12f31ff42fbe3f401ab5;hpb=d59f1c74c62ad3706d50707bb68758d88fbed006;p=helm.git

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 a01c225ee..7f0a71a8c 100644
--- 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,15 @@ 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.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_empty_labels (l) (n):
+      (𝐞) = l∗∗n → 𝟎 = n.
+#l #n @(nat_ind_succ … n) -n //
+#n #_ <labels_succ #H0 destruct
+qed-.