∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {f : ℕ → α → β} {ys : Vector β n} {xs : Vector α (n + 1)} {b : β},
  Vector.mapIdx f xs = ys.push b ↔ ∃ a zs, xs = zs.push a ∧ Vector.mapIdx f zs = ys ∧ f n a = b