for_all_list_map' {A B : Type} (P : B -> Type) (f : A -> B) : forall l, for_all (P o f) l -> for_all P (list_map f l). Proof. by apply for_all_list_map. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum