∀ {α : Type u} {β : Type v} (as : Array α) (motive : ℕ → Array β → Prop),
  (∀ (i : ℕ) (bs : Array β), i < as.size → (∀ (__do_lift : β), motive (i + 1) (bs.push __do_lift)) → motive i bs) →
    (∀ (i : ℕ) (bs : Array β), ¬i < as.size → motive i bs) → ∀ (i : ℕ) (bs : Array β), motive i bs