simp only [zipWith_cons]
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x✝ : SizedArray α n
y✝ : SizedArray β n
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : zipWith y x (flip f) = zipWith x y f
⊢ zipWith (cons b y) (cons a x) (flip f) = zipWith (cons a x) (cons b y) f
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x✝ : SizedArray α n
y✝ : SizedArray β n
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : zipWith y x (flip f) = zipWith x y f
⊢ cons (flip f b a) (zipWith y x (flip f)) = cons (f a b) (zipWith x y f)