proposition: Lemma flat_map_incl (f: X -> list Y) A B: A ⊆ B -> flat_map f A ⊆ flat_map f B.
proof: Proof. intros H x [y []] % in_flat_map. eapply in_flat_map; exists y; intuition auto. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)