English
Let α be a nonempty type and l an arbitrary list of α. Then the value produced by the last-index version equals the value obtained by extracting the last element from the last option, i.e. l.getLastI = (l.getLast?).iget.
Русский
Пусть α нес пустой тип, а l — произвольный список элементов α. Тогда значение, получаемое через последнюю позицию, равно значению, получаемому извлечением из последнего элемента опции: l.getLastI = (l.getLast?).iget.
LaTeX
$$$\forall l:\, List\;\alpha,\; l.getLastI = (l.getLast?).iget$$$
Lean4
theorem getLastI_eq_getLast? [Inhabited α] : ∀ l : List α, l.getLastI = l.getLast?.iget
| [] => by simp [getLastI]
| [_] => rfl
| [_, _] => rfl
| [_, _, _] => rfl
| _ :: _ :: c :: l => by simp [getLastI, getLastI_eq_getLast? (c :: l)]
