∀ {α : Type u_1} {cmp : α → α → Ordering} {motive : (a : Batteries.RBNode α) → Batteries.RBNode.WF cmp a → Prop}
  {motive_1 : {a : Batteries.RBNode α} → (t : Batteries.RBNode.WF cmp a) → Batteries.RBNode.WF.below t → Prop}
  {a : Batteries.RBNode α} {t : Batteries.RBNode.WF cmp a} (t_1 : Batteries.RBNode.WF.below t),
  (∀ {t : Batteries.RBNode α} {c : Batteries.RBColor} {n : ℕ} (a : Batteries.RBNode.Ordered cmp t)
      (a_1 : t.Balanced c n), motive_1 ⋯ ⋯) →
    (∀ {t : Batteries.RBNode α} {a : α} (a_1 : Batteries.RBNode.WF cmp t) (ih : Batteries.RBNode.WF.below a_1)
        (a_ih : motive t a_1), motive_1 ⋯ ⋯) →
      (∀ {t : Batteries.RBNode α} {cut : α → Ordering} (a : Batteries.RBNode.WF cmp t)
          (ih : Batteries.RBNode.WF.below a) (a_ih : motive t a), motive_1 ⋯ ⋯) →
        motive_1 t t_1