proposition: Fact flat_map_flat_map X Y Z (f : X -> list Y) (g : Y -> list Z) l : flat_map g (flat_map f l) = flat_map (fun x => flat_map g (f x)) l.
proof: Proof. induction l; simpl; auto. rewrite flat_map_app; f_equal; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)