{A : Type} {n : trunc_index} (P : A -> Type) (l : list A) : for_all (fun x => IsTrunc n (P x)) l -> IsTrunc n (for_all P l). Proof. induction l as [|x l IHl]; simpl. - destruct n; exact _. - intros [Hx Hl]. apply IHl in Hl. exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum