∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited γ] {f : α → β → Option γ}
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      Std.Internal.List.getValue! k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
        ((Std.Internal.List.getValue? k l).pbind fun v h => f (Std.Internal.List.getKey k l ⋯) v).get!