English
For a list formed by cons a onto l, the IsChain condition is equivalent to a relatedness condition between a and the first element of l and a chain condition inside l.
Русский
Для цепи, начинающейся с головы a над списком, равносильно условие, что a связан с первым элементом списка, и далее цепь внутри tail.
LaTeX
$$$IsChain\\, R\\,(a :: l) \\iff (\\forall h: 0 < length l, R\\ a\\ (get l ⟨0, h⟩)) \\land \\forall i, (i < l.length - 1) \\,→ \\, R\\ (get l ⟨i\\, \\_⟩) \\ (get l ⟨i+1, \\_⟩) $$$
Lean4
theorem isChain_cons_iff_get {R} {a : α} {l : List α} :
IsChain R (a :: l) ↔
(∀ h : 0 < length l, R a (get l ⟨0, h⟩)) ∧
∀ (i : ℕ) (h : i < l.length - 1), R (get l ⟨i, by cutsat⟩) (get l ⟨i + 1, by cutsat⟩) :=
by cases l <;> grind [isChain_iff_get]
