list_filter@{u v|} {A : Type@{u}} (l : list A) (P : A -> Type@{v}) (dec : forall x, Decidable (P x)) : list A := match l with | nil => nil | x :: l => if dec x then x :: list_filter l P dec else list_filter l P dec end.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum