α : Type u_1
t : RBNode α
v : α
p : Path α
⊢ toList
      (match t with
      | nil => insertNew p v
      | node c a v_1 b => fill p (node c a v b)) =
    listL p ++ (toList (setRoot v t) ++ listR p)
α : Type u_1
t : RBNode α
v : α
p : Path α
⊢ toList (insert p t v) = withList p (toList (setRoot v t))
simp [insert]
no goals
α : Type u_1
t : RBNode α
v : α
p : Path α
⊢ toList
      (match t with
      | nil => insertNew p v
      | node c a v_1 b => fill p (node c a v b)) =
    listL p ++ (toList (setRoot v t) ++ listR p)
split <;> simp [setRoot]