English
There is a case-analysis principle for FreeMonoid: a predicate C on FreeMonoid α is determined by its value at 1 and a rule for of x * xs; specifically, C(xs) equals the value given by the List.casesOn decomposition.
Русский
Существует принцип разбиения на случаи для FreeMonoid: предикат C на FreeMonoid α определяется по значению на единице и правилу для of x * xs; то есть C(xs) эквивалентно разложению List.casesOn.
LaTeX
$$$$\\forall C:\\\, FreeMonoid(\\alpha) \\to \\text{Sort},\\\\ xs:\\ FreeMonoid(\\alpha),\\ h_0:\\ C(1),\\ ih:\\forall x,xs, C( of x * xs),\\ C(xs) = List.casesOn(xs,h_0,ih). $$$$
Lean4
/-- A version of `List.cases_on` for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of
`[]` and `x :: xs`. -/
@[to_additive (attr := elab_as_elim, cases_eliminator) /-- A version of `List.casesOn` for `FreeAddMonoid` using `0` and
`FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`. -/
]
def casesOn {C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1) (ih : ∀ x xs, C (of x * xs)) : C xs :=
List.casesOn xs h0 ih
