proposition: Lemma Exists_concat A P (ls : list (list A)) : Exists P (concat ls) <-> Exists (Exists P) ls.
proof: Proof. induction ls as [|l ls IHls]. - cbn. now rewrite Exists_nil. - cbn. now rewrite Exists_app, Exists_cons, IHls. Qed.
imports: PeanoNat