{A : Type} (l l' : list A) (P : A -> Type) (dec : forall x, Decidable (P x)) : list_filter (l ++ l') P dec = list_filter l P dec ++ list_filter l' P dec. Proof. simple_list_induction l a l IHl. - reflexivity. - simpl; destruct (dec a); trivial. simpl; f_ap. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum