English
Let α be a type. Suppose C is a property that, for every natural number n, assigns a statement to each vector of length n. If for every list l of elements of α the statement C holds for the vector built from l, i.e. C(⟨l, rfl⟩), then for every n and every v : Vector α n we have C v. In other words, a property that is determined by the underlying list can be proved for all vectors by proving it for all lists of the corresponding length.
Русский
Пусть α — множество. Пусть C — свойство, задающее утверждение о векторах каждой длины. Если для каждого списка l элементов α верно, что C ⟨l, rfl⟩, тогда для любого n и любого v : Vector α n верно C v. Другими словами, свойство, зависящее только от соответствующего списка, можно доказать для всех векторов, доказав его для всех списков заданной длины.
LaTeX
$$$\\forall \\alpha,\\ \\forall C:\\, (\\forall l:\\,\\text{List}(\\alpha),\\ C\\langle l, rfl\\rangle)\\Rightarrow (\\forall n:\\mathbb{N},\\ \\forall v:\\text{Vector}(\\alpha,n),\\ C\\,v)$$$
Lean4
/-- Elimination rule for `Vector`. -/
@[elab_as_elim]
def elim {α} {C : ∀ {n}, Vector α n → Sort u} (H : ∀ l : List α, C ⟨l, rfl⟩) {n : ℕ} : ∀ v : Vector α n, C v
| ⟨l, h⟩ =>
match n, h with
| _, rfl => H l
