proposition: Lemma Forall_map A B (f : A -> B) P l : Forall P (map f l) <-> Forall (fun x => P (f x)) l.
proof: Proof. induction l as [|a l IHl]; cbn. - now rewrite !Forall_nil_iff. - now rewrite !Forall_cons_iff, IHl. Qed.
imports: PeanoNat