∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.TreeMap.Raw α β compare},
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α}, compare ((t.modify k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq