∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.containsKey k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
        true ↔
      ∃ (h : Std.Internal.List.containsKey k l = true), (f k (Std.Internal.List.getValueCast k l h)).isSome = true)