α : Type u_1
c : RBColor
a : RBNode α
x : α
b : RBNode α
⊢ toList a ++ x :: foldr (fun x x_1 => x :: x_1) b [] = toList a ++ x :: toList b
α : Type u_1
c : RBColor
a : RBNode α
x : α
b : RBNode α
⊢ toList (node c a x b) = toList a ++ x :: toList b
rw [toList, foldr, foldr_cons]
no goals
α : Type u_1
c : RBColor
a : RBNode α
x : α
b : RBNode α
⊢ toList a ++ x :: foldr (fun x x_1 => x :: x_1) b [] = toList a ++ x :: toList b
rfl