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