∀ {α : Type u} {δ : Type w} [inst : Ord α] (k : α) (size : ℕ) (k' : α) (v' : δ)
  (l r : Std.DTreeMap.Internal.Impl α fun x => δ),
  Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.inner size k' v' l r) k =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.get? l k
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.get? r k
    | Ordering.eq => some v'