proposition: Lemma nodup_map_filter l : NoDup l -> (forall x y z, In x l -> In y l -> f x = Some z -> f y = Some z -> x = y) -> NoDup (map_filter l).
proof: Proof. Proof using. induction l; ins; desf; rewrite ?nodup_cons, ?in_map_filter in *; desf; splits; eauto. by intro; desf; eauto; rewrite (H0 a a0 b) in H; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation