English
If a chain starts with a and ends with b, and p propagates backwards, then p holds at a given final predicate at b.
Русский
Если цепь начинается с a и заканчивается b, и p распространяется назад, то p держится в начале a.
LaTeX
$$$IsChain\\, R\\,(a::l) \\rightarrow Eq ((a::l).getLast ...) b \\rightarrow (\\forall x, R x y \\Rightarrow p y \\Rightarrow p x) \\Rightarrow p b \\Rightarrow p a$$$
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 at `a`.
That is, we can propagate the predicate all the way up the chain.
-/
@[elab_as_elim]
theorem backwards_cons_induction_head (p : α → Prop) (l : List α) (h : IsChain r (a :: l))
(hb : getLast (a :: l) (cons_ne_nil _ _) = b) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : p b) : p a :=
(IsChain.backwards_cons_induction p l h hb carries final) _ mem_cons_self
