English
Applying a function to each element commutes with snoc: map f (xs.snoc x) = (map f xs).snoc (f x).
Русский
Применение функции ко всем элементам commuting с добавлением элемента в конец: map f (xs.snoc x) = (map f xs).snoc (f x).
LaTeX
$$$\text{map } f (xs.snoc x) = (\text{map } f xs).snoc (f x)$$$
Lean4
@[simp]
theorem map_snoc {f : α → β} : map f (xs.snoc x) = (map f xs).snoc (f x) := by induction xs <;> simp_all