X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fbasics%2Flist.ma;h=94ef847b00c4aa70ba0ed10f5b97b8d6c3146082;hb=c57405141d26ac2215a07b05d27a16a691dda50e;hp=b5664d1341e13562510002b40d4720f22165d3ac;hpb=cf89508024f0a19023bb1bac343012d54e860d9d;p=helm.git

diff --git a/helm/software/matita/nlibrary/basics/list.ma b/helm/software/matita/nlibrary/basics/list.ma
index b5664d134..94ef847b0 100644
--- a/helm/software/matita/nlibrary/basics/list.ma
+++ b/helm/software/matita/nlibrary/basics/list.ma
@@ -39,7 +39,7 @@ ndefinition not_nil: ∀A:Type.list A → Prop ≝
 
 ntheorem nil_cons:
   ∀A:Type.∀l:list A.∀a:A. a::l ≠ [].
-  #A; #l; #a; #Heq; nchange with (not_nil ? (a::l));
+  #A; #l; #a; napply nmk; #Heq; nchange with (not_nil ? (a::l));
   nrewrite > Heq; //;
 nqed.
 
@@ -73,13 +73,16 @@ ntheorem associative_append:
  ∀A:Type.associative (list A) (append A).
 #A; #l1; #l2; #l3; nelim l1; nnormalize; //; nqed.
 
+(* deleterio per auto 
 ntheorem cons_append_commute:
   ∀A:Type.∀l1,l2:list A.∀a:A.
     a :: (l1 @ l2) = (a :: l1) @ l2.
-//; nqed.
+//; nqed. *)
 
 ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
-/2/; nqed.
+#A; #a; #l; #l1; napply sym_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.