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