English
Let Γ be a nonempty type and L be a ListBlank over Γ. Then the 0-th element of L equals its head: L.nth(0) = L.head.
Русский
Пусть Γ — непустой тип, а L — ListBlank над Γ. Тогда нулевой элемент L равен его голове: L.nth(0) = L.head.
LaTeX
$$$\forall {\Gamma} [Inhabited(\Gamma)]\,(l : ListBlank(\Gamma)),\ l.nth(0) = l.head$$$
Lean4
@[simp]
theorem nth_zero {Γ} [Inhabited Γ] (l : ListBlank Γ) : l.nth 0 = l.head :=
by
conv => lhs; rw [← ListBlank.cons_head_tail l]
exact Quotient.inductionOn' l.tail fun l ↦ rfl