English
Recurse on an n+1 tuple by splitting into the initial n-tuple and the last element; this is an elimination/induction principle.
Русский
Рекурсивно по (n+1)-кортежу разбивая его на начальный n-кортеж и последний элемент; это принцип элиминации/индукции.
LaTeX
$$$\\text{snocInduction} : \\text{EliminationPrinciple} (n, q, P) \\text{ with base and step }$$$
Lean4
/-- Recurse on an `n+1`-tuple by splitting it its initial `n`-tuple and its last element. -/
@[elab_as_elim, inline]
def snocCases {P : (∀ i : Fin n.succ, α i) → Sort*} (h : ∀ xs x, P (Fin.snoc xs x)) (x : ∀ i : Fin n.succ, α i) : P x :=
_root_.cast (by rw [Fin.snoc_init_self]) <| h (Fin.init x) (x <| Fin.last _)
