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