{α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Lean.RBNode α β → (x : α) → β x → Sort u_3) →
      (x : Lean.RBNode α β) →
        (x_1 : α) →
          (x_2 : β x_1) →
            ((kx : α) → (vx : β kx) → motive Lean.RBNode.leaf kx vx) →
              ((a : Lean.RBNode α β) →
                  (ky : α) →
                    (vy : β ky) →
                      (b : Lean.RBNode α β) →
                        (kx : α) → (vx : β kx) → motive (Lean.RBNode.node Lean.RBColor.red a ky vy b) kx vx) →
                ((a : Lean.RBNode α β) →
                    (ky : α) →
                      (vy : β ky) →
                        (b : Lean.RBNode α β) →
                          (kx : α) → (vx : β kx) → motive (Lean.RBNode.node Lean.RBColor.black a ky vy b) kx vx) →
                  motive x x_1 x_2