English
The Word obtained from a NeWord by the toWord construction is compatible with the original toList and the Word constraints; in particular, structural witnesses coincide with the Word construction.
Русский
Слово, полученное из NeWord через преобразование toWord, согласуется с исходным toList и ограничениями Word; структуры совпадают с конструкцией Word.
LaTeX
$$$$\\text{toWord}(w)\\text{ satisfies the same toList as } w,\\text{ and the witnesses agree.}$$$$
Lean4
/-- One can replace the first letter in a non-empty reduced word by an element of the same
group -/
def replaceHead : ∀ {i j : ι} (x : M i) (_hnotone : x ≠ 1) (_w : NeWord M i j), NeWord M i j
| _, _, x, h, singleton _ _ => singleton x h
| _, _, x, h, append w₁ hne w₂ => append (replaceHead x h w₁) hne w₂
