proposition: Lemma flat_map_in_incl f a A: a ∈ A -> f a ⊆ flat_map f A.
proof: Proof. revert A; eapply in_ind; cbn; intuition (auto with datatypes). Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)