simp[toOptionVec]
case succ
α : Type u_1
n : ℕ
ih : ∀ {v : Fin n → Option α}, toOptionVec v = none ↔ ∃ i, v i = none
v : Fin (n + 1) → Option α
⊢ toOptionVec v = none ↔ ∃ i, v i = none
case succ
α : Type u_1
n : ℕ
ih : ∀ {v : Fin n → Option α}, toOptionVec v = none ↔ ∃ i, v i = none
v : Fin (n + 1) → Option α
⊢ (∀ (a : Fin n → α), toOptionVec (v ∘ succ) = some a → v 0 = none) ↔ ∃ i, v i = none