English
A propagation principle along concatenation allows deriving p for all elements of l ++ [b] from a starting point a and a base case.
Русский
Принцип распространения вдоль конкатенации позволяет получить свойство для всех элементов l ++ [b] от двойного основания.
LaTeX
$$$\\forall p\\;\\forall l:\\, IsChain\\, R (l++[b]) \\rightarrow Eq (head (l++[b])) a \\rightarrow (\\forall x,y,\\dots) \\Rightarrow \\forall i \\in l++[b], p i$$$
Lean4
theorem concat_induction (p : α → Prop) (l : List α) (h : IsChain r (l ++ [b]))
(hb : head (l ++ [b]) (concat_ne_nil _ _) = a) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) :
∀ i ∈ l ++ [b], p i :=
h.induction _ _ carries (fun _ => hb ▸ initial)
