∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β}, (t.insertIfNew k v)[a]? = if cmp k a = Ordering.eq ∧ k ∉ t then some v else t[a]?