{A : Type} (P : A -> Type) l : (forall x, InList x l -> P x) -> for_all P l. Proof. simple_list_induction l h t IHl; intros H; cbn; trivial; split. - apply H. by left. - apply IHl. intros y i. apply H. by right. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum