theorem Array.sizeOf_head?_of_mem {α : Type u_1} {a : α} {as' : Array α} [SizeOf α] {as : Array α} (h : as.head? = some (a, as')) : sizeOf a < sizeOf as

theorem Array.sizeOf_head?_of_tail {α : Type u_1} {a : α} {as' : Array α} [SizeOf α] {as : Array α} (h : as.head? = some (a, as')) : sizeOf as' < sizeOf as

theorem Array.sizeOf_dropLast_cons {α : Type u_1} [SizeOf α] (a : α) (as : List α) : sizeOf (a :: as).dropLast < sizeOf (a :: as)

theorem Array.sizeOf_dropLast_non_empty {α : Type u_1} [SizeOf α] (as : List α) (h : 0 < as.length) : sizeOf as.dropLast < sizeOf as

theorem Array.sizeOf_pop_non_empty {α : Type u_1} [SizeOf α] (as : Array α) (h : 0 < as.toList.length) : sizeOf as.pop < sizeOf as

theorem Array.sizeOf_pop? {α : Type u_1} {a : α} {as' : Array α} [SizeOf α] {as : Array α} (h : as.pop? = some (a, as')) : sizeOf as' < sizeOf as

theorem Array.size_one {α : Type u_1} (a : α) : #[a].size = 1

theorem Array.default_size_zero {α : Type u_1} (arr : Array α) (h : arr = default) : arr.size = 0

theorem Array.non_empty_of_last? {α : Type u_1} {last : α} (arr : Array α) (h : arr.last? = some last) : 0 < arr.size

theorem Array.pop?_of_last? {α : Type u_1} {last : α} (arr : Array α) (h : arr.last? = some last) : ∃ (arr' : Array α), arr.pop? = some (last, arr')

theorem Array.pop?_of_non_empty {α : Type u_1} (arr : Array α) (h : 0 < arr.size) : ∃ (arr' : Array α), ∃ (last : α), arr.pop? = some (last, arr')

theorem Array.last?_eq_getLast {α : Type u_1} {last : α} (a : Array α) (h1 : a.last? = some last) (h2 : a.toList ≠ []) : a.toList.getLast h2 = last

theorem Array.lt_of_pop?_eq_last? {α : Type u_1} {last : α} {arr' arr : Array α} (h : arr.pop? = some (last, arr')) : 0 < arr.toList.length

theorem Array.get_last_of_pop? {α : Type u_1} {last : α} {arr' arr : Array α} (h1 : arr.pop? = some (last, arr')) (h2 : arr.toList.length - 1 < arr.toList.length) : arr.toList.get ⟨arr.toList.length - 1, h2⟩ = last

theorem Array.concat_of_pop? {α : Type u_1} {last : α} {arr' arr : Array α} (h : arr.pop? = some (last, arr')) : arr.toList = arr'.toList ++ [last]

theorem Array.get_eq_get?_some {α : Type u_1} {i : Nat} {a : α} {as : Array α} (hlt : i < as.size) (h : a = as[i]) : as[i]? = some a