exact IH
case cons.succ
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : Nat.succ i < n✝ + 1
⊢ (zipWith x y f)[i] = f x[i] y[i]
no goals