α : Type u_1
x : α
r : RBNode α
s : RBNode.Stream α
⊢ x :: (RBNode.toList r ++ foldr (fun x x_1 => x :: x_1) s []) =
    x :: RBNode.toList r ++ foldr (fun x x_1 => x :: x_1) s []
α : Type u_1
x : α
r : RBNode α
s : RBNode.Stream α
⊢ toList (cons x r s) = x :: RBNode.toList r ++ toList s
rw [toList, toList, foldr, RBNode.foldr_cons]
no goals
α : Type u_1
x : α
r : RBNode α
s : RBNode.Stream α
⊢ x :: (RBNode.toList r ++ foldr (fun x x_1 => x :: x_1) s []) =
    x :: RBNode.toList r ++ foldr (fun x x_1 => x :: x_1) s []
rfl