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

diff --git a/helm/software/matita/nlibrary/basics/list.ma b/helm/software/matita/nlibrary/basics/list.ma
index 3d41b946c..94ef847b0 100644
--- a/helm/software/matita/nlibrary/basics/list.ma
+++ b/helm/software/matita/nlibrary/basics/list.ma
@@ -80,7 +80,7 @@ ntheorem cons_append_commute:
 //; nqed. *)
 
 ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
-#A; #a; #l; #l1; napply symmetric_eq.
+#A; #a; #l; #l1; napply sym_eq.
 napply associative_append.
 (* /2/; *) nqed.