proposition: Lemma in_flatten_iff A (x: A) ll : In x (flatten ll) <-> exists l, In l ll /\ In x l.
proof: Proof. induction ll; ins. by split; ins; desf. rewrite in_app_iff, IHll; clear; split; ins; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation