X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Flist_rcons.ma;h=66910e1a90fd775370bb047504a0a521f0108422;hb=2e4a7c54ef77c10cb1cef4b59518c473245ea935;hp=2cf2e23bf07f662e9563fc2e0dccb9274e1ff8d7;hpb=12dc655b7f5321b33b93a310d53e23e60e090caa;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
index 2cf2e23bf..66910e1a9 100644
--- 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-.