proposition: Lemma Exists_map A B (f : A -> B) P l : Exists P (map f l) <-> Exists (fun x => P (f x)) l.
proof: Proof. induction l as [|a l IHl]. - cbn. now rewrite Exists_nil. - cbn. now rewrite ?Exists_cons, IHl. Qed.
imports: PeanoNat