proposition: Lemma elem_of_list_intersection_with f l k x : x ∈ list_intersection_with f l k ↔ ∃ x1 x2, x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x.
proof: Proof. split. - induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|]. intros Hx. setoid_rewrite elem_of_cons. cut ((∃ x2, x2 ∈ k ∧ f x1 x2 = Some x) ∨ x ∈ list_intersection_with f l k); [naive_solver|]. clear IH. revert Hx. generalize (list_intersection_with f l k). induction k; simpl; [by auto|]. case_match; setoid_rewrite elem_of_cons; naive_solver. - intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1 l|x1 ? l ? IH]; simpl. + generalize (list_intersection_with f l k). induction Hx2; simpl; [by rewrite Hx; left |]. case_match; simpl; try setoid_rewrite elem_of_cons; auto. + generalize (IH Hx). clear Hx IH Hx2. generalize (list_intersection_with f l k). induction k; simpl; intros; [done|]. case_match; simpl; rewrite ?elem_of_cons; auto. Qed.
imports: stdpp(options)