∀ {α : Type u_1} {c₀ : Batteries.RBColor} {n₀ : ℕ} {c : Batteries.RBColor} {n : ℕ} {path : Batteries.RBNode.Path α}
  {t : Batteries.RBNode α},
  Batteries.RBNode.Path.Balanced c₀ n₀ path c n → t.Balanced c n → path.ins t = (path.fill t).setBlack