X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Flist.ma;h=a486fd39ae1fbf2cdcf0096331b5a7759358368b;hb=ef07f57f5fb5bc34897fdef44987e6a154206807;hp=6dc752d65ad5b4aa84d5b22e2d6a8b9f0654e084;hpb=77479649510792efe4d9cbff508e118360862594;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list.ma b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
index 6dc752d65..a486fd39a 100644
--- 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-.