∀ {α : Type u_1} (l : Batteries.RBNode α) (v : α) (r' a : Batteries.RBNode α) (y : α) (b : Batteries.RBNode α) (z : α)
  (c : Batteries.RBNode α),
  (∀ (a : Batteries.RBNode α) (x : α) (b : Batteries.RBNode α),
      l = Batteries.RBNode.node Batteries.RBColor.red a x b → False) →
    ∀ (a_1 : Batteries.RBNode α) (x : α) (b_1 : Batteries.RBNode α),
      Batteries.RBNode.node Batteries.RBColor.red a_1 x b_1 = l.reverse →
        (Batteries.RBNode.node Batteries.RBColor.red (Batteries.RBNode.node Batteries.RBColor.black l v a) y
              (b.balance2 z c.setRed)).reverse =
          Batteries.RBNode.node Batteries.RBColor.red r' v (Batteries.RBNode.node Batteries.RBColor.black a_1 x b_1)