English
Two-step induction expresses a recursive equality that expands a two-element seed into a full list via a consistent recurrence.
Русский
Двухступенчатая индукция выражает рекурсивное равенство, которое расширяет начальные два элемента в полный список по устойчивому правилу.
LaTeX
$$$\forall {\alpha}, {\motive}, (x,y, xs)\; \text{twoStepInduction }\; Nil\; singleton\; cons_cons\; (x::y::xs) = cons_cons\; x\; y\; xs\; (twoStepInduction\; Nil\; singleton\; cons_cons\; xs)\; (\lambda z, twoStepInduction\; Nil\; singleton\; cons_cons\; (z::xs))$$$
Lean4
@[simp]
theorem twoStepInduction_cons_cons {motive : (l : List α) → Sort*} (x y : α) (xs : List α) (nil : motive [])
(singleton : ∀ x, motive [x]) (cons_cons : ∀ x y xs, motive xs → (∀ y, motive (y :: xs)) → motive (x :: y :: xs)) :
twoStepInduction nil singleton cons_cons (x :: y :: xs) =
cons_cons x y xs (twoStepInduction nil singleton cons_cons xs)
(fun y => twoStepInduction nil singleton cons_cons (y :: xs)) :=
twoStepInduction.eq_3 ..
