∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k a : α}
  {h₁ : a ∈ t.insert k}, (t.insert k).get a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then k else t.get a ⋯