X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_labels.ma;h=e7e1391da6313ed92d874bad2ec09bdce551870e;hb=3729defa81f91b5f1259d628299bce9dbc5bfb7f;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..e7e1391da 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma
@@ -40,3 +40,11 @@ lemma labels_succ (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-.