proposition: Lemma Forall_concat A P (ls : list (list A)) : Forall P (concat ls) <-> Forall (Forall P) ls.
proof: Proof. induction ls as [|l ls IHls]; cbn. - now rewrite !Forall_nil_iff. - now rewrite Forall_app, Forall_cons_iff, IHls. Qed.
imports: PeanoNat