∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] {f : (a : α) → β a → γ a} {k : α} (h : t.WF)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.map f t) = true},
  (Std.DTreeMap.Internal.Impl.map f t).getKey k h' = t.getKey k ⋯