no goals
α : Type u_1
α✝ : Type u_2
f : α✝ → α → α✝
init : α✝
t : RBNode.Stream α
⊢ foldl f init t = List.foldl f init (toList t)
induction t generalizing init <;> simp [-List.foldl] <;> simp [*, RBNode.foldl_eq_foldl_toList]