∀ {α : Type u_1} {c : Batteries.RBColor} {n : ℕ} {cmp : α → α → Ordering} {p : Batteries.RBNode.Path α} {v : α}
  {t : Batteries.RBNode α},
  t.Balanced c n →
    Batteries.RBNode.zoom (cmp v) t = (Batteries.RBNode.nil, p) →
      (Batteries.RBNode.insert cmp t v).toList = p.withList [v]