have h_range_size : (Array.range n).size = n := Array.range_size
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ False
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Array.range n).size = n
⊢ False