α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ toList l ++ x :: foldr List.cons r [] = toList l ++ x :: toList r
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ toList (node s l x r) = toList l ++ x :: toList r
rw [toList, foldr, foldr_cons_eq_toList]
no goals
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ toList l ++ x :: foldr List.cons r [] = toList l ++ x :: toList r
rfl