+#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.
+#A;#l1; #l2; #P; ncases l1; nnormalize;//;
+#a; #l3; #heq; ndestruct;
+nqed.
+
+ntheorem nil_to_nil: ∀A.∀l1,l2:list A.
+ l1@l2 = [] → l1 = [] ∧ l2 = [].
+#A; #l1; #l2; #isnil; napply (nil_append_elim A l1 l2);/2/;
+nqed.
+
+(* ierators *)