- paths and left residuals: forth case of the equivalence proved!

[helm.git] / matita / matita / contribs / lambda / background / preamble.ma

diff --git a/matita/matita/contribs/lambda/background/preamble.ma b/matita/matita/contribs/lambda/background/preamble.ma
index 01874eb726f90ccc8cf006254540b6c303547b33..769ffa5a366838ff9dd5660e3440d72f1a540cdd 100644 (file)
--- a/matita/matita/contribs/lambda/background/preamble.ma
+++ b/matita/matita/contribs/lambda/background/preamble.ma
@@ -87,6 +87,10 @@ notation > "◊"
   non associative with precedence 90
   for @{'nil}.
 
+lemma list_inv: ∀A. ∀l:list A. ◊ = l ∨ ∃∃a0,l0. a0 :: l0 = l.
+#A * /2 width=1/ /3 width=3/
+qed-.
+
 definition map_cons: ∀A. A → list (list A) → list (list A) ≝ λA,a.
                      map … (cons … a).