∀ {α : Type u_1} (v : α) (motive : Batteries.RBNode α → Batteries.RBNode α → Batteries.RBNode α → Prop),
  (∀ (l a : Batteries.RBNode α) (x : α) (b : Batteries.RBNode α),
      motive l (Batteries.RBNode.node Batteries.RBColor.red a x b)
        (Batteries.RBNode.node Batteries.RBColor.red l v (Batteries.RBNode.node Batteries.RBColor.black a x b))) →
    (∀ (l : Batteries.RBNode α),
        (∀ (a : Batteries.RBNode α) (x : α) (b : Batteries.RBNode α),
            l = Batteries.RBNode.node Batteries.RBColor.red a x b → False) →
          ∀ (a : Batteries.RBNode α) (x : α) (b : Batteries.RBNode α),
            motive (Batteries.RBNode.node Batteries.RBColor.black a x b) l
              ((Batteries.RBNode.node Batteries.RBColor.red a x b).balance1 v l)) →
      (∀ (l : Batteries.RBNode α),
          (∀ (a : Batteries.RBNode α) (x : α) (b : Batteries.RBNode α),
              l = Batteries.RBNode.node Batteries.RBColor.red a x b → False) →
            ∀ (a : Batteries.RBNode α) (x : α) (b : Batteries.RBNode α) (y : α) (c : Batteries.RBNode α),
              motive
                (Batteries.RBNode.node Batteries.RBColor.red a x (Batteries.RBNode.node Batteries.RBColor.black b y c))
                l
                (Batteries.RBNode.node Batteries.RBColor.red (a.setRed.balance1 x b) y
                  (Batteries.RBNode.node Batteries.RBColor.black c v l))) →
        (∀ (l : Batteries.RBNode α),
            (∀ (a : Batteries.RBNode α) (x : α) (b : Batteries.RBNode α),
                l = Batteries.RBNode.node Batteries.RBColor.red a x b → False) →
              ∀ (l_1 : Batteries.RBNode α),
                (∀ (a : Batteries.RBNode α) (x : α) (b : Batteries.RBNode α),
                    l_1 = Batteries.RBNode.node Batteries.RBColor.black a x b → False) →
                  (∀ (a : Batteries.RBNode α) (x : α) (b : Batteries.RBNode α) (y : α) (c : Batteries.RBNode α),
                      l_1 =
                          Batteries.RBNode.node Batteries.RBColor.red a x
                            (Batteries.RBNode.node Batteries.RBColor.black b y c) →
                        False) →
                    motive l_1 l (Batteries.RBNode.node Batteries.RBColor.red l_1 v l)) →
          ∀ (l r : Batteries.RBNode α), motive l r (l.balRight v r)