have : ∀ i, v i.succ = some (z i) := ih.mp hs
case succ.some.some
α : 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
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
⊢ a :> z = w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)
case succ.some.some
α : 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
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
this : ∀ (i : Fin n), v i.succ = some (z i)
⊢ a :> z = w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)