fact: Fixpoint map_filter l := match l with | nil => nil | x :: l => match f x with | None => map_filter l | Some b => b :: map_filter l end end.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation