split
case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (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 inr.isTrue
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x

case inr.isFalse
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x