proposition: Lemma elem_of_list_union l k x : x ∈ list_union l k ↔ x ∈ l ∨ x ∈ k.
proof: Proof. unfold list_union. rewrite elem_of_app, elem_of_list_difference. intuition. case (decide (x ∈ k)); intuition. Qed.
imports: stdpp(options)