{α : Type u} →
  {n : ℕ} →
    {motive : Vector α n → Sort u_1} →
      (t : Vector α n) →
        ((toArray : Array α) → (size_toArray : toArray.size = n) → motive (Vector.mk toArray size_toArray)) → motive t