update in ground

[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 00faad83dc2af5462773b9ef7ba0fc592ed623c1..bfbc0e986dba994d0f6e33f9d2e7e06880b2fa42 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
@@ -51,6 +51,12 @@ lemma eq_inv_list_empty_rcons (A):
 elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
 qed-.
 
+lemma eq_inv_list_rcons_empty (A):
+      ∀l,a. l⨭{A}a = ⓔ → ⊥.
+#A #l #a #H0
+elim (eq_inv_list_append_empty … H0) -H0 #_ #H0 destruct
+qed-.
+
 (* Advanced inversions ******************************************************)
 
 lemma eq_inv_list_rcons_bi (A):