∀ {α : Type u_1} (x : Batteries.RBNode.Path α),
  x.listR =
    match x with
    | Batteries.RBNode.Path.root => []
    | Batteries.RBNode.Path.left c parent v r => v :: r.toList ++ parent.listR
    | Batteries.RBNode.Path.right c l v parent => parent.listR