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