simp only [Array.range, flip] at ih
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Array.range n)[x] = x
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x