∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n},
  (xs.push a).attach =
    (Vector.map
          (fun x =>
            match x with
            | ⟨x, h⟩ => ⟨x, ⋯⟩)
          xs.attach).push
      ⟨a, ⋯⟩