∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst p.snd) l).isEmpty = false ↔
      ∃ k,
        ∃ (h : Std.Internal.List.containsKey k l = true),
          f (Std.Internal.List.getKey k l h) (Std.Internal.List.getValue k l h) = true)