∀ {α : Type u_1} {cut : α → Ordering} {t' : Batteries.RBNode α} {path' : Batteries.RBNode.Path α}
  {c₀ : Batteries.RBColor} {n₀ : ℕ} {path : Batteries.RBNode.Path α},
  let funType_1 := fun {t} {path} {c} {n} x x_1 =>
    Batteries.RBNode.zoom cut t path = (t', path') →
      ∃ c n, t'.Balanced c n ∧ Batteries.RBNode.Path.Balanced c₀ n₀ path' c n;
  ∀
    (motive :
      (n : ℕ) →
        (c : Batteries.RBColor) →
          (t : Batteries.RBNode α) →
            (x : t.Balanced c n) →
              Batteries.RBNode.Balanced.below (motive := fun {t} {c} {n} x =>
                  ∀ {path : Batteries.RBNode.Path α} (x_1 : Batteries.RBNode.Path.Balanced c₀ n₀ path c n),
                    funType_1 x x_1)
                  x →
                Batteries.RBNode.Path.Balanced c₀ n₀ path c n → Prop)
    (n : ℕ) (c : Batteries.RBColor) (t : Batteries.RBNode α) (x : t.Balanced c n)
    (below :
      Batteries.RBNode.Balanced.below (motive := fun {t} {c} {n} x =>
        ∀ {path : Batteries.RBNode.Path α} (x_1 : Batteries.RBNode.Path.Balanced c₀ n₀ path c n), funType_1 x x_1) x)
    (x_1 : Batteries.RBNode.Path.Balanced c₀ n₀ path c n),
    (∀ (hp : Batteries.RBNode.Path.Balanced c₀ n₀ path Batteries.RBColor.black 0),
        motive 0 Batteries.RBColor.black Batteries.RBNode.nil ⋯ ⋯ hp) →
      (∀ (n : ℕ) (x y : Batteries.RBNode α) (v : α) (ha : x.Balanced Batteries.RBColor.black n)
          (hb : y.Balanced Batteries.RBColor.black n)
          (hp : Batteries.RBNode.Path.Balanced c₀ n₀ path Batteries.RBColor.red n)
          (ih :
            Batteries.RBNode.Balanced.below (motive := fun {t} {c} {n} x =>
              ∀ {path : Batteries.RBNode.Path α} (x_2 : Batteries.RBNode.Path.Balanced c₀ n₀ path c n), funType_1 x x_2)
              ha)
          (a_ih :
            ∀ {path : Batteries.RBNode.Path α}
              (x_2 : Batteries.RBNode.Path.Balanced c₀ n₀ path Batteries.RBColor.black n), funType_1 ha x_2)
          (ih_1 :
            Batteries.RBNode.Balanced.below (motive := fun {t} {c} {n} x =>
              ∀ {path : Batteries.RBNode.Path α} (x_2 : Batteries.RBNode.Path.Balanced c₀ n₀ path c n), funType_1 x x_2)
              hb)
          (a_ih_1 :
            ∀ {path : Batteries.RBNode.Path α}
              (x : Batteries.RBNode.Path.Balanced c₀ n₀ path Batteries.RBColor.black n), funType_1 hb x),
          motive n Batteries.RBColor.red (Batteries.RBNode.node Batteries.RBColor.red x v y) ⋯ ⋯ hp) →
        (∀ (x : Batteries.RBNode α) (c₁ : Batteries.RBColor) (n : ℕ) (y : Batteries.RBNode α) (c₂ : Batteries.RBColor)
            (v : α) (ha : x.Balanced c₁ n) (hb : y.Balanced c₂ n)
            (hp : Batteries.RBNode.Path.Balanced c₀ n₀ path Batteries.RBColor.black (n + 1))
            (ih :
              Batteries.RBNode.Balanced.below (motive := fun {t} {c} {n} x =>
                ∀ {path : Batteries.RBNode.Path α} (x_2 : Batteries.RBNode.Path.Balanced c₀ n₀ path c n),
                  funType_1 x x_2)
                ha)
            (a_ih :
              ∀ {path : Batteries.RBNode.Path α} (x_2 : Batteries.RBNode.Path.Balanced c₀ n₀ path c₁ n),
                funType_1 ha x_2)
            (ih_1 :
              Batteries.RBNode.Balanced.below (motive := fun {t} {c} {n} x =>
                ∀ {path : Batteries.RBNode.Path α} (x_2 : Batteries.RBNode.Path.Balanced c₀ n₀ path c n),
                  funType_1 x x_2)
                hb)
            (a_ih_1 :
              ∀ {path : Batteries.RBNode.Path α} (x : Batteries.RBNode.Path.Balanced c₀ n₀ path c₂ n), funType_1 hb x),
            motive (n + 1) Batteries.RBColor.black (Batteries.RBNode.node Batteries.RBColor.black x v y) ⋯ ⋯ hp) →
          motive n c t x below x_1