{A B : Type} (P : A -> Type) (Q : B -> Type) (f : A -> B) (Hf : forall x, P x -> Q (f x)) : forall l, for_all P l -> for_all Q (list_map f l). Proof. simple_list_induction l x l IHl; simpl; trivial. intros [Hx Hl]. split; auto. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum