ntheorem nil_cons:
∀A:Type.∀l:list A.∀a:A. a::l ≠ [].
- #A; #l; #a; #Heq; nchange with (not_nil ? (a::l));
+ #A; #l; #a; napply nmk; #Heq; nchange with (not_nil ? (a::l));
nrewrite > Heq; //;
nqed.
∀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.
-/2/; nqed.
+#A; #a; #l; #l1; napply sym_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.