English
Let Γ be a nonempty type and l a finite list of elements of Γ. Then the nth element of the ListBlank constructed from l is exactly the nth element of l, i.e. (ListBlank.mk(l)).nth(n) = l.getI(n) for every n ∈ ℕ.
Русский
Пусть Γ — непустой тип, и l — конечный список элементов Γ. Тогда n-й элемент ListBlank, полученного из l, равен n‑му элементу самого списка, то есть (ListBlank.mk(l)).nth(n) = l.getI(n) для всякого n ∈ ℕ.
LaTeX
$$$\forall {\Gamma} [Inhabited(\Gamma)]\, (l : List(\Gamma)) (n : \mathbb{N}),\ (ListBlank.mk(l)).nth\,n = l.getI\,n$$$
Lean4
@[simp]
theorem nth_mk {Γ} [Inhabited Γ] (l : List Γ) (n : ℕ) : (ListBlank.mk l).nth n = l.getI n :=
rfl
