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