proposition: Lemma in_map_filter x l : In x (map_filter l) <-> exists a, f a = Some x /\ In a l.
proof: Proof. Proof using. induction l; ins; desf; ins; try (rewrite IHn; clear IHn); intuition; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation