∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β a → Bool},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (List.filter (fun p => f p.fst p.snd) l)