English
An induction principle: to prove a property for all words, it suffices to prove it for empty word and prove closure under smul.
Русский
Индуктивная схема по слову: свойство для всех слов доказывается, если верно для пустого слова и при закрытии относительно smul.
LaTeX
$$$$ \\text{smul\_induction} : \\forall motive,\\ motive\\ empty \\land (\\forall i m w, motive w \\to motive (of m \\cdot w)) \\to \\forall w, motive w $$$$
Lean4
@[elab_as_elim]
theorem smul_induction {motive : Word M → Prop} (empty : motive empty)
(smul : ∀ (i) (m : M i) (w), motive w → motive (of m • w)) (w : Word M) : motive w := by
induction w using consRecOn with
| empty => exact empty
| cons _ _ _ _ _ ih =>
rw [cons_eq_smul]
exact smul _ _ _ ih
