update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / list_rcons.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
index 2cf2e23bf07f662e9563fc2e0dccb9274e1ff8d7..66910e1a90fd775370bb047504a0a521f0108422 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
@@ -41,3 +41,11 @@ lemma list_append_rcons_sn (A):
 lemma list_append_rcons_dx (A):
       ∀l1,l2,a. l1 ⨁ l2 ⨭ a = l1 ⨁{A} (l2 ⨭ a).
 // qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_list_empty_rcons (A):
+      ∀l,a. ⓔ = l⨭{A}a → ⊥.
+#A #l #a #H
+elim (eq_inv_list_empty_append … H) -H #_ #H destruct
+qed-.