English
If p is a path from a to b, then the list obtained by prepending b to p.toList, namely b :: p.toList, is a chain with the same chain relation: for each consecutive pair, there exists a morphism from the second to the first.
Русский
Пусть p — путь от a до b. Тогда список, полученный прибавлением головы b к p.toList, то есть b :: p.toList, образует цепь по тому же отношению: между соседними вершинами существует морфизм от второй к первой.
LaTeX
$$$\\forall {V} [Quiver\\ V] {a,b:V} (p:Path\\ a\\ b),\\ (b :: p.toList)\\ IsChain\\left(\\lambda x\\ y. \\exists f:\\ y\\to x\\right).$$
Lean4
theorem isChain_cons_toList_nonempty : ∀ {b} (p : Path a b), (b :: p.toList).IsChain (fun x y => Nonempty (y ⟶ x))
| _, nil => .singleton _
| _, cons p f => p.isChain_cons_toList_nonempty.cons_cons ⟨f⟩
