∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l sofar : List ((a : α) × β a)) (k : α),
  Std.Internal.List.interSmallerFn l sofar k =
    match Std.Internal.List.getEntry? k l with
    | some kv' => Std.Internal.List.insertEntry kv'.fst kv'.snd sofar
    | none => sofar