∀ {α : Type u_1} {n : ℕ} (xs : Array α) (ys : Vector α n)
  (motive : (∃ (h : xs.size = n), (Vector.mk xs h).Perm ys) → Prop) (h : ∃ (h : xs.size = n), (Vector.mk xs h).Perm ys),
  (∀ (h : xs.size = n) (p : (Vector.mk xs h).Perm ys), motive ⋯) → motive h