∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a fallback : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.getKeyD a fallback =
    if compare k a = Ordering.eq then fallback else t.getKeyD a fallback