English
There is a recursor for lists that expands a list into a function mapping to its elements; it is usable with induction on lists via ofFnRec.
Русский
Существует рекурсор для списков, который разворачивает список в функцию отображения к его элементам; им можно пользоваться для индукции по спискам через ofFnRec.
LaTeX
$$$ \\text{ofFnRec} : \\forall C:\\ List(\\alpha) \\to \\mathrm{Sort}*,\\ldots \\,$ (recursor statement for lists).$$
Lean4
/-- A recursor for lists that expands a list into a function mapping to its elements.
This can be used with `induction l using List.ofFnRec`. -/
@[elab_as_elim]
def ofFnRec {C : List α → Sort*} (h : ∀ (n) (f : Fin n → α), C (List.ofFn f)) (l : List α) : C l :=
cast (congr_arg C l.ofFn_get) <| h l.length l.get
