proposition: Lemma filterP_map A (d : A -> Prop) B (f : B -> A) l : filterP d (map f l) = map f (filterP (f ↓₁ d) l).
proof: Proof. induction l; ins; desf; ins; f_equal; ins. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation