fact: Fixpoint filterP A (f: A -> Prop) l := match l with | nil => nil | x :: l => if excluded_middle_informative (f x) then x :: filterP f l else filterP f l end.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation