simp only [Array.range, Nat.fold, flip, Array.size_push, Nat.succ.injEq]
n : Nat
ih : (Array.range n).size = n
⊢ (Array.range (n + 1)).size = n + 1
n : Nat
ih : (Array.range n).size = n
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size = n