α : Type u_1
t : RBNode.Stream α
l : List α
⊢ foldr (fun x x_1 => x :: x_1) t l = foldr (fun x x_1 => x :: x_1) t [] ++ l
α : Type u_1
t : RBNode.Stream α
l : List α
⊢ foldr (fun x x_1 => x :: x_1) t l = toList t ++ l
unfold toList
case h
α : Type u_1
t : RBNode.Stream α
l : List α
⊢ foldr (fun x x_1 => x :: x_1) t [] ++ l = foldr (fun x x_1 => x :: x_1) t l
α : Type u_1
t : RBNode.Stream α
l : List α
⊢ foldr (fun x x_1 => x :: x_1) t l = foldr (fun x x_1 => x :: x_1) t [] ++ l
apply Eq.symm
no goals
case h
α : Type u_1
t : RBNode.Stream α
l : List α
⊢ foldr (fun x x_1 => x :: x_1) t [] ++ l = foldr (fun x x_1 => x :: x_1) t l
induction t <;> simp [*, foldr, RBNode.foldr_cons]