simpa using hs
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
hs : toOptionVec (v ∘ succ) = none
⊢ ∃ i, v i.succ = none
no goals