∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [Std.LawfulEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false} {km : α},
      Std.Internal.List.maxKey l he = km ↔
        Std.Internal.List.containsKey km l = true ∧
          ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare k km).isLE = true