From cb4b0c887ba703b7949656d5b72b5f94756a77bd Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 2 Nov 2011 10:58:34 +0000
Subject: [PATCH] The proof of append_cons used transitive_eq, not indexed. If
 other cases will present we shall reindex it.

---
 matita/matita/lib/basics/list.ma | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma
index 8b0449987..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.
-- 
2.39.2