{A : Type} (P : A -> Type) (l : list A) : forall (x : A), InList x l -> P x -> list_exists P l. Proof. simple_list_induction l x l IHl. 1: trivial. simpl; intros y H p; revert H. apply functor_sum. - exact (fun r => r^ # p). - intros H. by apply (IHl y). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum