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..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,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-.