{α : Type u_1} →
  {n : ℕ} →
    (lo hi : ℕ) →
      (motive : { m // lo ≤ m ∧ m ≤ hi } × Vector α n → Sort u_2) →
        (x : { m // lo ≤ m ∧ m ≤ hi } × Vector α n) →
          ((mid : ℕ) → (hmid : lo ≤ mid ∧ mid ≤ hi) → (as : Vector α n) → motive (⟨mid, hmid⟩, as)) → motive x