∀ {α : Type u_1} {j i : ℕ} {a b : Array α},
  ¬-1 * ↑i + ↑a.size ≤ 0 →
    ¬↑i + -1 * ↑(min j (a ++ b).size) ≤ 0 →
      ((a ++ b).extract i j).size = (a.extract i j).size →
        ∀ (w : ℕ), w + 1 ≤ ((a ++ b).extract i j).size → w < (a.extract i j).size