English
Every i ∈ Fin2(succ n) is either the zero element or the successor of some j ∈ Fin2 n, with a dependent case split: H1 for fz and H2 for fs n.
Русский
Любой элемент Fin2(succ n) равен либо нулю, либо переходу к следующему элементу, т. е. fs n, с разбором по случаям: H1 при fz и H2 при fs n.
LaTeX
$$$\forall n, \forall C : Fin2 (succ n) \to \mathrm{Sort} u,\ (H1 : C(\mathrm{fz})) \ (H2 : \forall n, C(\mathrm{fs} n)) \Rightarrow \forall i : \mathrm{Fin2}(n+1), C(i)$$$
Lean4
/-- Define a dependent function on `Fin2 (succ n)` by giving its value at
zero (`H1`) and by giving a dependent function on the rest (`H2`). -/
@[elab_as_elim]
protected def cases' {n} {C : Fin2 (succ n) → Sort u} (H1 : C fz) (H2 : ∀ n, C (fs n)) : ∀ i : Fin2 (succ n), C i
| fz => H1
| fs n => H2 n
