//; nqed.
ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
-/2/; nqed.
+#A; #a; #l; #l1; napply symmetric_eq.
+napply associative_append.
+(* /2/; *) nqed.
ntheorem nil_append_elim: ∀A.∀l1,l2: list A.∀P: list A → list A → Prop.
l1@l2 = [] → P (nil A) (nil A) → P l1 l2.