English
Given a chain along l ++ [b] ending at b, and a predicate that propagates backwards, you get p along l from the tail.
Русский
Условие цепи вдоль l ++ [b] и перенос предиката назад дают p вдоль l от хвоста.
LaTeX
$$$\\forall p\\, l \\; h,\\ IsChain\\, r\\, (l++[b]) \\rightarrow (\\forall x, R x y \\Rightarrow p y \\Rightarrow p x) \\Rightarrow p b \\Rightarrow \\forall i \\in l, p i$$$
Lean4
/-- Given a chain from `a` to `b`, and a predicate true at `b`, if `r x y → p y → p x` then
the predicate is true everywhere in the chain and at `a`.
That is, we can propagate the predicate up the chain.
-/
theorem backwards_concat_induction (p : α → Prop) (l : List α) (h : IsChain r (l ++ [b]))
(carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : p b) : ∀ i ∈ l, p i := fun _ hi =>
h.backwards_induction _ _ carries (fun _ => getLast_concat ▸ final) _ (mem_append_left _ hi)
