∀ {α : Type u_1} {β : α → Type u_2} (motive : Lean.RBNode α β → Sort u_3) (lchild : Lean.RBNode α β) (key : α)
  (val : β key) (rchild : Lean.RBNode α β)
  (h_1 :
    (lchild : Lean.RBNode α β) →
      (key : α) →
        (val : β key) → (rchild : Lean.RBNode α β) → motive (Lean.RBNode.node Lean.RBColor.red lchild key val rchild))
  (h_2 : (x : Lean.RBNode α β) → motive x),
  (match Lean.RBNode.node Lean.RBColor.red lchild key val rchild with
    | Lean.RBNode.node Lean.RBColor.red lchild key val rchild => h_1 lchild key val rchild
    | x => h_2 x) =
    h_1 lchild key val rchild