∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α fun x => β) (fallback : α × β),
  Std.DTreeMap.Internal.Impl.Const.getEntryLED k t fallback =
    (Std.DTreeMap.Internal.Impl.Const.getEntryLE? k t).getD fallback