{A : Type} {P : A -> Type} {l : list A} {p : for_all P l} : length (list_sigma P l p) = length l. Proof. revert p; simple_list_induction l x l IHl; intro p. 1: reflexivity. destruct p as [Hx Hl]. cbn; f_ap. apply IHl. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum