English
Coinductive principle for All: given motive on sequences, base case, and step, one can deduce p x for every x in s.
Русский
Коиндуктивный принцип All: для мотивы на последовательностях, базового случая и шага можно получить свойство p для каждого элемента x в s.
LaTeX
$$$\forall s\,\forall motive\,\forall base\,\forall step,\ \text{If base holds and step ensures} \ p, \ \forall x\in s,\ p x$$$
Lean4
/-- Coinductive principle for `All`. -/
theorem all_coind {s : Seq α} {p : α → Prop} (motive : Seq α → Prop) (base : motive s)
(step : ∀ hd tl, motive (.cons hd tl) → p hd ∧ motive tl) : ∀ x ∈ s, p x :=
by
apply all_of_get
intro n
have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right) n
rw [← head_dropn]
generalize s.drop n = s' at this
cases s' with
| nil => simp
| cons hd tl => simp [(step hd tl this).left]
