∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ [inst : Inhabited α] {k : α} {f : β → β},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).getKey! k = if k ∈ t then k else default