∀ {α : Type u} {β : α → Type v} (color : Lean.RBColor) (lchild : Lean.RBNode α β) (key : α) (val : β key)
  (rchild : Lean.RBNode α β) (color_1 : Lean.RBColor) (lchild_1 : Lean.RBNode α β) (key_1 : α) (val_1 : β key_1)
  (rchild_1 : Lean.RBNode α β),
  (Lean.RBNode.node color lchild key val rchild = Lean.RBNode.node color_1 lchild_1 key_1 val_1 rchild_1) =
    (color = color_1 ∧ lchild = lchild_1 ∧ key = key_1 ∧ val ≍ val_1 ∧ rchild = rchild_1)