proposition: Lemma map_filter_app (l l' : list A) : map_filter (l ++ l') = map_filter l ++ map_filter l'.
proof: Proof. Proof using. induction l; ins; desf; ins; congruence. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation