∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (k : α) (fallback : (a : α) × β a),
  t.getEntryD k fallback =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => fallback
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r =>
      match compare k k' with
      | Ordering.lt => l.getEntryD k fallback
      | Ordering.gt => r.getEntryD k fallback
      | Ordering.eq => ⟨k', v'⟩