proposition: Lemma concat_nil_Forall A : forall (l : list (list A)), concat l = nil <-> Forall (fun x => x = nil) l.
proof: Proof. intro l; induction l as [|a l IHl]; simpl; split; intros Hc; auto. - apply app_eq_nil in Hc. constructor; firstorder. - inversion Hc; subst; simpl. now apply IHl. Qed.
imports: PeanoNat