∀ {α : Type u_1},
  let funType_1 := fun {t} {c} {n} x => 2 ^ Batteries.RBNode.depthLB c n ≤ t.size + 1;
  ∀
    (motive :
      (n : ℕ) →
        (c : Batteries.RBColor) →
          (t : Batteries.RBNode α) → (x : t.Balanced c n) → Batteries.RBNode.Balanced.below x → Prop)
    (n : ℕ) (c : Batteries.RBColor) (t : Batteries.RBNode α) (x : t.Balanced c n)
    (below : Batteries.RBNode.Balanced.below x),
    (∀ (a : Unit), motive 0 Batteries.RBColor.black Batteries.RBNode.nil ⋯ ⋯) →
      (∀ (n : ℕ) (x y : Batteries.RBNode α) (v : α) (hl : x.Balanced Batteries.RBColor.black n)
          (hr : y.Balanced Batteries.RBColor.black n) (ih : Batteries.RBNode.Balanced.below hl) (a_ih : funType_1 hl)
          (ih_1 : Batteries.RBNode.Balanced.below hr) (a_ih_1 : funType_1 hr),
          motive n Batteries.RBColor.red (Batteries.RBNode.node Batteries.RBColor.red x v y) ⋯ ⋯) →
        (∀ (x : Batteries.RBNode α) (c₁ : Batteries.RBColor) (n : ℕ) (y : Batteries.RBNode α) (c₂ : Batteries.RBColor)
            (v : α) (hl : x.Balanced c₁ n) (hr : y.Balanced c₂ n) (ih : Batteries.RBNode.Balanced.below hl)
            (a_ih : funType_1 hl) (ih_1 : Batteries.RBNode.Balanced.below hr) (a_ih_1 : funType_1 hr),
            motive (n + 1) Batteries.RBColor.black (Batteries.RBNode.node Batteries.RBColor.black x v y) ⋯ ⋯) →
          motive n c t x below