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