update 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 a01c225ee50b1c9575bb12f31ff42fbe3f401ab5..e7e1391da6313ed92d874bad2ec09bdce551870e 100644 (file)
--- 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-.