English
Let α be a type and n a natural number. For any a ∈ α and any v ∈ List.Vector α n, the Sym element obtained by prepending a to the class of v equals the class of the vector obtained by prepending a to v. In other words, the Sym cons operation matches the underlying vector prepending.
Русский
Пусть α — тип, n — натуральное число. Для любого a ∈ α и вектора v ∈ List.Vector α n элемент Sym, получаемый добавлением a в начало представления v, равен представлению вектора, полученного добавлением a в начало v. Иными словами, операция cons в Sym согласуется с добавлением в векторе.
LaTeX
$$$ \mathrm{Sym.cons}(a, \mathrm{Sym.ofVector}(v)) = \mathrm{Sym.ofVector}(\mathrm{Vector.cons}(a,v)). $$$
Lean4
theorem cons_of_coe_eq (a : α) (v : List.Vector α n) : a ::ₛ (↑v : Sym α n) = ↑(a ::ᵥ v) :=
Subtype.ext <| by
cases v
rfl
