∀ {α : Type u_1} (l : Batteries.RBNode α) (v : α) (r r' l' : Batteries.RBNode α),
  r' = r.reverse →
    l' = l.reverse →
      (Batteries.RBNode.node Batteries.RBColor.red l v r).reverse = Batteries.RBNode.node Batteries.RBColor.red r' v l'