English
Every NeWord M i j determines a corresponding Word M by forgetting the nonempty-ness constraint and preserving the sequence of letters; this construction yields a valid Word whose underlying list is the same as the NeWord’s toList and whose structural witnesses satisfy the Word conditions.
Русский
Каждому NeWord M i j соответствует соответствующее Word M, получаемое путём игнорирования ограничения на ненулевость и сохранения последовательности букв; полученный Word имеет тот же список и удовлетворяет условиям Word.
LaTeX
$$$$\\text{toWord}: \\text{NeWord } M\\, i\\, j \\to \\text{Word } M,$$$$
Lean4
/-- The `Word M` represented by a `NeWord M i j` -/
def toWord {i j} (w : NeWord M i j) : Word M where
toList := w.toList
ne_one := by
induction w
· simpa only [toList, List.mem_singleton, ne_eq, forall_eq]
· intro l h
simp only [toList, List.mem_append] at h
cases h <;> aesop
chain_ne := by
induction w
· exact List.isChain_singleton _
· refine List.IsChain.append (by assumption) (by assumption) ?_
intro x hx y hy
rw [toList_getLast?, Option.mem_some_iff] at hx
rw [toList_head?, Option.mem_some_iff] at hy
subst hx
subst hy
assumption
