no goals
m : Type u_1 → Type u_2
α : Type u_3
a✝ : Type u_1
f : a✝ → α → m a✝
init : a✝
inst✝¹ : Monad m
inst✝ : LawfulMonad m
t : RBNode α
⊢ foldlM f init t = List.foldlM f init (toList t)
induction t generalizing init <;> simp [*]