α : Type u_1
t : RBNode α
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 α
l : List α
⊢ foldr (fun x x_1 => x :: x_1) t l = toList t ++ l
unfold toList
no goals
α : Type u_1
t : RBNode α
l : List α
⊢ foldr (fun x x_1 => x :: x_1) t l = foldr (fun x x_1 => x :: x_1) t [] ++ l
induction t generalizing l with
| nil => rfl
| node _ a _ b iha ihb => rw [foldr, foldr, iha, iha (_::_), ihb]; simp
no goals
case nil
α : Type u_1
l : List α
⊢ foldr (fun x x_1 => x :: x_1) nil l = foldr (fun x x_1 => x :: x_1) nil [] ++ l
rfl
case node
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
iha : ∀ (l : List α), foldr (fun x x_1 => x :: x_1) a l = foldr (fun x x_1 => x :: x_1) a [] ++ l
ihb : ∀ (l : List α), foldr (fun x x_1 => x :: x_1) b l = foldr (fun x x_1 => x :: x_1) b [] ++ l
l : List α
⊢ foldr (fun x x_1 => x :: x_1) a [] ++ v✝ :: (foldr (fun x x_1 => x :: x_1) b [] ++ l) =
    foldr (fun x x_1 => x :: x_1) a [] ++ v✝ :: foldr (fun x x_1 => x :: x_1) b [] ++ l
case node
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
iha : ∀ (l : List α), foldr (fun x x_1 => x :: x_1) a l = foldr (fun x x_1 => x :: x_1) a [] ++ l
ihb : ∀ (l : List α), foldr (fun x x_1 => x :: x_1) b l = foldr (fun x x_1 => x :: x_1) b [] ++ l
l : List α
⊢ foldr (fun x x_1 => x :: x_1) (node c✝ a v✝ b) l = foldr (fun x x_1 => x :: x_1) (node c✝ a v✝ b) [] ++ l
rw [foldr, foldr, iha, iha (_::_), ihb]
no goals
case node
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
iha : ∀ (l : List α), foldr (fun x x_1 => x :: x_1) a l = foldr (fun x x_1 => x :: x_1) a [] ++ l
ihb : ∀ (l : List α), foldr (fun x x_1 => x :: x_1) b l = foldr (fun x x_1 => x :: x_1) b [] ++ l
l : List α
⊢ foldr (fun x x_1 => x :: x_1) a [] ++ v✝ :: (foldr (fun x x_1 => x :: x_1) b [] ++ l) =
    foldr (fun x x_1 => x :: x_1) a [] ++ v✝ :: foldr (fun x x_1 => x :: x_1) b [] ++ l
simp