∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (i : ℕ) (x : α),
  xs.insertIdx! i x =
    if x_1 : i ≤ n then xs.insertIdx i x x_1
    else
      have this := { default := xs.push x };
      panicWithPosWithDecl "Init.Data.Vector.Basic" "Vector.insertIdx!" 404 4 "index out of bounds"