∀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.
-#A; #a; #l; #l1; napply symmetric_eq.
+#A; #a; #l; #l1; napply sym_eq.
napply associative_append.
(* /2/; *) nqed.