]> matita.cs.unibo.it Git - helm.git/commitdiff
symmetric_eq -> sym_eq
authorAndrea Asperti <andrea.asperti@unibo.it>
Tue, 23 Mar 2010 15:59:10 +0000 (15:59 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Tue, 23 Mar 2010 15:59:10 +0000 (15:59 +0000)
From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

helm/software/matita/nlibrary/basics/list.ma

index 3d41b946c73a7929a227c529ab313f7d3a273c8e..94ef847b00c4aa70ba0ed10f5b97b8d6c3146082 100644 (file)
@@ -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.