English
Equality of two cons-constructed words reduces to equality of heads and tails under the appropriate equivalences; the constructors are compatible with the equality relation.
Русский
Сравнение двух слов, образованных через cons, сводится к равенству голов и хвостов при подходящем эквивалентном преобразовании; конструкторы совместимы с отношением равенства.
LaTeX
$$$ \\mathrm{cons}\\, m\\, w\, hmw\, h1 = \\mathrm{cons}\\, m_1\\, w_1\, hmw_1\, h1_1 \\Rightarrow \\cdots$$$
Lean4
/-- Construct a new `Word` without any reduction. The underlying list of
`cons m w _ _` is `⟨_, m⟩::w` -/
@[simps]
def cons {i} (m : M i) (w : Word M) (hmw : w.fstIdx ≠ some i) (h1 : m ≠ 1) : Word M :=
{ toList := ⟨i, m⟩ :: w.toList,
ne_one := by
simp only [List.mem_cons]
rintro l (rfl | hl)
· exact h1
· exact w.ne_one l hl
chain_ne := w.chain_ne.cons' (fstIdx_ne_iff.mp hmw) }
