update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list.ma b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
index 6dc752d65ad5b4aa84d5b22e2d6a8b9f0654e084..a486fd39ae1fbf2cdcf0096331b5a7759358368b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
@@ -35,3 +35,12 @@ rec definition list_all A (R:predicate A) (l:list A) on l ≝ match l with
 [ list_empty       ⇒ ⊤
 | list_lcons hd tl ⇒ ∧∧ R hd & list_all A R tl
 ].
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_list_lcons_bi (A) (a1) (a2) (l1) (l2):
+      a1⨮l1 = a2⨮{A}l2 →
+      ∧∧ a1 = a2 & l1 = l2.
+#A #a1 #a2 #l1 #l2 #H0 destruct
+/2 width=1 by conj/
+qed-.