no goals
α : Type u_1
t : RBNode α
p : Path α
⊢ toList (ins p t) = withList p (toList t)
match p with
| .root | .left red .. | .right red .. | .left black .. | .right black .. =>
  simp [ins, ins_toList]
no goals
α : Type u_1
t : RBNode α
p : Path α
l✝ : RBNode α
v✝ : α
parent✝ : Path α
⊢ toList (ins (right black l✝ v✝ parent✝) t) = withList (right black l✝ v✝ parent✝) (toList t)
simp [ins, ins_toList]