From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 19 Feb 2010 07:30:16 +0000 (+0000)
Subject: New proofs.
X-Git-Tag: make_still_working~3037
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=35a0b2aaeb0413fedbe7de94973167c98222e30e;p=helm.git

New proofs.
---

diff --git a/helm/software/matita/nlibrary/basics/list.ma b/helm/software/matita/nlibrary/basics/list.ma
index b5664d134..92eddc705 100644
--- a/helm/software/matita/nlibrary/basics/list.ma
+++ b/helm/software/matita/nlibrary/basics/list.ma
@@ -79,7 +79,9 @@ ntheorem cons_append_commute:
 //; nqed.
 
 ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
-/2/; nqed.
+#A; #a; #l; #l1; napply symmetric_eq.
+napply associative_append.
+(* /2/; *) nqed.
 
 ntheorem nil_append_elim: ∀A.∀l1,l2: list A.∀P: list A → list A → Prop. 
   l1@l2 = [] → P (nil A) (nil A) → P l1 l2.