English
Prepending a new last element to a RelSeries does not change its head: (p.snoc newLast rel).head = p.head.
Русский
Добавление нового последнего элемента слева не меняет головы последовательности: (p.snoc newLast rel).head = p.head.
LaTeX
$$$ (p.\text{snoc } newLast\ rel).\text{head} = p.\text{head} $$$
Lean4
@[simp]
theorem head_snoc (p : RelSeries r) (newLast : α) (rel : p.last ~[r] newLast) : (p.snoc newLast rel).head = p.head := by
delta snoc; rw [head_append]