∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α}
  {k fallback : α}, k ∈ t → (t.insertManyIfNewUnit l).getKeyD k fallback = t.getKeyD k fallback