∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeMap.Raw α Unit cmp},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (l : List α), (t₁.insertManyIfNewUnit l).Equiv (t₂.insertManyIfNewUnit l)