∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (e : (a : α) × β a) (l : List ((a : α) × β a)),
  Std.Internal.List.minKey? (e :: l) =
    some
      (match Std.Internal.List.minKey? l with
      | none => e.fst
      | some w => if (compare e.fst w).isLE = true then e.fst else w)