proposition: Lemma elem_of_list_intersection l k x : x ∈ list_intersection l k ↔ x ∈ l ∧ x ∈ k.
proof: Proof. split; induction l; simpl; repeat case_decide; rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence. Qed.
imports: stdpp(options)