English
If a relation series p ends with an element that matches the head of q, then the first element of their joined series smash(p,q,h) is the first element of p.
Русский
Если последовательность p оканчивается на элемент, совпадающий с началом последовательности q, то первый элемент объединённой последовательности smash(p,q,h) совпадает с первым элементом p.
LaTeX
$$$$ (\\text{smash}(p,q,h)).\\text{head} = p.\\text{head}. $$$$
Lean4
@[simp]
theorem head_smash {p q : RelSeries r} (h : p.last = q.head) : (smash p q h).head = p.head :=
by
obtain ⟨_ | _, _⟩ := p
· simpa [Fin.addCases] using h.symm
dsimp only [smash, head]
exact Fin.addCases_left 0
