{A : Type} {P : A -> Type} (l : list A) : for_all P l -> forall x, InList x l -> P x. Proof. simple_list_induction l x l IHl. - contradiction. - intros [Hx Hl] y [-> | i]. + exact Hx. + apply IHl. 1: exact Hl. exact i. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum