English
Two walks are equal if they have the same vertex sequence: if for all k, p.getVert k = q.getVert k, then p = q.
Русский
Два хода совпадают тогда и только тогда, когда совпадают их последовательности вершин: если для всех k p.getVert k = q.getVert k, то p = q.
LaTeX
$$$ (\\forall k,\\ p.getVert k = q.getVert k) \\rightarrow p = q $$$
Lean4
theorem ext_support {u v} {p q : G.Walk u v} (h : p.support = q.support) : p = q := by
induction q with
| nil =>
rw [← nil_iff_eq_nil, nil_iff_support_eq]
exact support_nil ▸ h
| cons ha q ih =>
cases p with
| nil => simp at h
| cons _ p =>
simp only [support_cons, List.cons.injEq, true_and] at h
apply List.getElem_of_eq at h
specialize h (i := 0) (by simp)
rw [List.getElem_zero, List.getElem_zero, p.head_support, q.head_support] at h
have : (p.copy h rfl).support = q.support := by simpa
simp [← ih this]
