α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ toList
      (match l, v, r with
      | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
      | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d)
      | a, x, b => node black a x b) =
    toList l ++ v :: toList r
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ toList (balance1 l v r) = toList l ++ v :: toList r
unfold balance1
no goals
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ toList
      (match l, v, r with
      | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
      | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d)
      | a, x, b => node black a x b) =
    toList l ++ v :: toList r
split <;> simp