X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Flib%2Fbasics%2Flist.ma;h=eaf89510a153c2f90e67c23c45caccf93a09f9d0;hb=fc7af5f9ea2cd4a876b8babc6b691136799e3c87;hp=21dd7e3d1aa57597da06b06b7ba2c1c192b84be2;hpb=a6602de6db0993a67c5b23aedb3c8fe1d484855f;p=helm.git

diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma
index 21dd7e3d1..eaf89510a 100644
--- a/matita/matita/lib/basics/list.ma
+++ b/matita/matita/lib/basics/list.ma
@@ -72,7 +72,7 @@ ntheorem cons_append_commute:
 //; nqed. *)
 
 theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
-/2/ qed.
+#A #a #l #l1 >associative_append // qed.
 
 theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. 
   l1@l2=[] → P (nil A) (nil A) → P l1 l2.
@@ -214,5 +214,5 @@ qed.
 
 lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
 #A #n elim n -n /2/
-#n #IHn * normalize /2/
+#n #IHn *; normalize /2/
 qed.