∀ {α : Type u_1} {β : α → Type u_2} (motive : Lean.RBNode α β → Lean.RBNode α β → Sort u_3) (a b : Lean.RBNode α β)
  (kx : α) (vx : β kx) (c : Lean.RBNode α β) (h_1 : (x : Lean.RBNode α β) → motive Lean.RBNode.leaf x)
  (h_2 : (x : Lean.RBNode α β) → motive x Lean.RBNode.leaf)
  (h_3 :
    (a : Lean.RBNode α β) →
      (kx : α) →
        (vx : β kx) →
          (b c : Lean.RBNode α β) →
            (ky : α) →
              (vy : β ky) →
                (d : Lean.RBNode α β) →
                  motive (Lean.RBNode.node Lean.RBColor.red a kx vx b) (Lean.RBNode.node Lean.RBColor.red c ky vy d))
  (h_4 :
    (a : Lean.RBNode α β) →
      (kx : α) →
        (vx : β kx) →
          (b c : Lean.RBNode α β) →
            (ky : α) →
              (vy : β ky) →
                (d : Lean.RBNode α β) →
                  motive (Lean.RBNode.node Lean.RBColor.black a kx vx b)
                    (Lean.RBNode.node Lean.RBColor.black c ky vy d))
  (h_5 :
    (a b : Lean.RBNode α β) →
      (kx : α) → (vx : β kx) → (c : Lean.RBNode α β) → motive a (Lean.RBNode.node Lean.RBColor.red b kx vx c))
  (h_6 :
    (a : Lean.RBNode α β) →
      (kx : α) → (vx : β kx) → (b c : Lean.RBNode α β) → motive (Lean.RBNode.node Lean.RBColor.red a kx vx b) c),
  (a = Lean.RBNode.leaf → False) →
    (∀ (a_1 : Lean.RBNode α β) (kx : α) (vx : β kx) (b : Lean.RBNode α β),
        a = Lean.RBNode.node Lean.RBColor.red a_1 kx vx b → False) →
      (match a, Lean.RBNode.node Lean.RBColor.red b kx vx c with
        | Lean.RBNode.leaf, x => h_1 x
        | x, Lean.RBNode.leaf => h_2 x
        | Lean.RBNode.node Lean.RBColor.red a kx vx b, Lean.RBNode.node Lean.RBColor.red c ky vy d =>
          h_3 a kx vx b c ky vy d
        | Lean.RBNode.node Lean.RBColor.black a kx vx b, Lean.RBNode.node Lean.RBColor.black c ky vy d =>
          h_4 a kx vx b c ky vy d
        | a, Lean.RBNode.node Lean.RBColor.red b kx vx c => h_5 a b kx vx c
        | Lean.RBNode.node Lean.RBColor.red a kx vx b, c => h_6 a kx vx b c) =
        h_5 a b kx vx c