∀ {α : Type u_1} {β : Type u_2} (init : β) (as : Array α),
  Array.SizeFitsUSize✝ as →
    ∀ (start stop : ℕ),
      (USize.ofNat (min start as.size)).toNat - (USize.ofNat (min stop (min start as.size))).toNat <
        (Array.replicate (min start as.size - min stop (min start as.size) + 1) init).size