exact dif_neg n.not_lt_zero
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array β
n : Nat
z : Array γ
⊢ (if h : n < size #[] then
      let a := #[][n];
      if h : n < size x then
        let b := x[n];
        zipWithAux f #[] x (n + 1) (push z (f a b))
      else z
    else z) =
    z
no goals