proposition: Lemma Forall_map@{uT uU} : forall (T : Type@{uT}) (U : Type@{uU}) (f : T -> U) P ls, Forall P (List.map f ls) <-> Forall (fun x => P (f x)) ls.
proof: Proof. induction ls; simpl. { split; intros; constructor. } { split; inversion 1; intros; subst; constructor; auto. apply IHls. auto. apply IHls. auto. } Qed.
imports: Coq.Lists.List ExtLib.Core.RelDec ExtLib.Structures.Monoid ExtLib.Structures.Reducible ExtLib.Tactics.Consider ExtLib.Tactics.Injection