α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ toList
      (match r with
      | node red b y c => node red l v (node black b y c)
      | r =>
        match l with
        | node black a x b => balance1 (node red a x b) v r
        | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
        | l => node red l v r) =
    toList l ++ v :: toList r
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ toList (balRight l v r) = toList l ++ v :: toList r
unfold balRight
case h_2
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
⊢ toList
      (match l with
      | node black a x b => balance1 (node red a x b) v r
      | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
      | l => node red l v r) =
    toList l ++ v :: toList r
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ toList
      (match r with
      | node red b y c => node red l v (node black b y c)
      | r =>
        match l with
        | node black a x b => balance1 (node red a x b) v r
        | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
        | l => node red l v r) =
    toList l ++ v :: toList r
split <;> simp
no goals
case h_2
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
⊢ toList
      (match l with
      | node black a x b => balance1 (node red a x b) v r
      | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
      | l => node red l v r) =
    toList l ++ v :: toList r
split <;> simp