fact: Definition take_first {elt} (f : M.key → elt → bool) (k : M.key) (e : elt) (x0 : option (M.key * elt)) := match x0 with | Some _ => x0 | None => if f k e then Some (k, e) else None end.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts