∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} {δ : Type w} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  t₁.Equiv t₂ → Std.TreeSet.foldlM f init t₁ = Std.TreeSet.foldlM f init t₂