∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {i : ℕ}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.entryAtIdx! i = t₂.entryAtIdx! i