Require PolyList.
Fixpoint append_list [A:Set;l:(list (list A))] : (list A) :=
Cases l of
| nil => (nil A)
| (cons La Lq) => (app La (append_list A Lq))
end.
Implicits append_list [1].
Lemma in_append_list : (A:Set;l:(list A);L:(list (list A)))
(In l L) -> (incl l (append_list L)).
NewInduction L; Simpl; Intros.
Elim H.
Elim H; Clear H; Intros.
Subst.
Auto with datatypes.
Auto with datatypes.
Qed.