∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] (f : Fin n → m α)
  (motive : (i : ℕ) → i ≤ n → (acc : Array α) → acc.size = i → m (Vector α n) → Prop),
  (∀ (acc : Array α) (h' : acc.size ≤ n) (h : acc.size < n),
      (∀ (__do_lift : α),
          motive (acc.size + 1) ⋯ (acc.push __do_lift) ⋯ (Vector.ofFnM.go✝ f (acc.size + 1) ⋯ (acc.push __do_lift) ⋯)) →
        motive acc.size h' acc ⋯ do
          let __do_lift ← f ⟨acc.size, h⟩
          Vector.ofFnM.go✝¹ f (acc.size + 1) ⋯ (acc.push __do_lift) ⋯) →
    (∀ (acc : Array α) (h' : acc.size ≤ n) (h : ¬acc.size < n), motive acc.size h' acc ⋯ (pure (Vector.mk acc ⋯))) →
      ∀ (i : ℕ) (h' : i ≤ n) (acc : Array α) (w : acc.size = i), motive i h' acc w (Vector.ofFnM.go✝² f i h' acc w)