fact: Definition list_intersection_with (f : A → A → option A) : list A → list A → list A := fix go l k := match l with | [] => [] | x :: l => foldr (λ y, match f x y with None => id | Some z => (z ::.) end) (go l k) k end.
imports: stdpp(options)