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