intros
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
⊢ ∀ (h : n < size x),
    (let a_1 := (cons a x)[n + 1];
      if h : n + 1 < size (cons b y) then
        let b_1 := (cons b y)[n + 1];
        zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
      else z) =
      let a := x[n];
      if h : n < size y then
        let b := y[n];
        zipWithAux f x y (n + 1) (push z (f a b))
      else z
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝ : n < size x
⊢ (let a_1 := (cons a x)[n + 1];
    if h : n + 1 < size (cons b y) then
      let b_1 := (cons b y)[n + 1];
      zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
    else z) =
    let a := x[n];
    if h : n < size y then
      let b := y[n];
      zipWithAux f x y (n + 1) (push z (f a b))
    else z