proposition: Fact in_concat_iff X (ll : list (list X)) x : In x (concat ll) <-> exists l, In x l /\ In l ll.
proof: Proof. rewrite <- (map_id ll) at 1. rewrite <- flat_map_concat_map, in_flat_map. firstorder. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)