∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k' v l r).get? k =
    match h : compare k k' with
    | Ordering.lt => l.get? k
    | Ordering.gt => r.get? k
    | Ordering.eq => some (cast ⋯ v)