{α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Lean.RBNode α β → α → Option (Sigma β) → Sort u_3) →
      (x : Lean.RBNode α β) →
        (x_1 : α) →
          (x_2 : Option (Sigma β)) →
            ((x : α) → (lb : Option (Sigma β)) → motive Lean.RBNode.leaf x lb) →
              ((color : Lean.RBColor) →
                  (a : Lean.RBNode α β) →
                    (ky : α) →
                      (vy : β ky) →
                        (b : Lean.RBNode α β) →
                          (x : α) → (lb : Option (Sigma β)) → motive (Lean.RBNode.node color a ky vy b) x lb) →
                motive x x_1 x_2