{A : Type} (P : A -> Type) (l : list A) : list_exists P l -> exists (x : A), InList x l /\ P x. Proof. simple_list_induction l x l IHl. 1: done. simpl. intros [Px | ex]. - exists x. by split; [left|]. - destruct (IHl ex) as [x' [H Px']]. exists x'. by split; [right|]. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum