no goals
m : Type u_1 → Type u_2
α : Type u_3
α✝ : Type u_1
f : α → α✝ → m (ForInStep α✝)
init : α✝
inst✝¹ : Monad m
inst✝ : LawfulMonad m
t : RBNode α
⊢ forIn.visit f t init = ForInStep.bindList f (toList t) (ForInStep.yield init)
induction t generalizing init <;> simp [*, forIn.visit]