unfold zipWith
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ zipWith (push x a) (push y b) f = push (zipWith x y f) (f a b)
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ mapIdx (fun i => f (push x a)[i]) (push y b) = push (mapIdx (fun i => f x[i]) y) (f a b)