{A : Type} (P : A -> Type) (l : list A) (p : for_all P l) : list {x : A & P x}. Proof. induction l as [|x l IHl] in p |- *. 1: exact nil. destruct p as [Hx Hl]. exact ((x; Hx) :: IHl Hl). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum