∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} [inst : NeZero (n + m)],
  (xs ++ ys).back =
    if h' : m = 0 then
      have this := ⋯;
      xs.back
    else
      have this := ⋯;
      ys.back