English
If every z dominated by x under R also dominates z under y, then replacing the head a of a chain by some b that preserves this implication yields another chain.
Русский
Если для всех z выполняется R(x,z) ⇒ R(y,z) и цепь имеет голову x, а также l, то цепь с головой y тоже является цепью.
LaTeX
$$$\\forall \\{\\alpha\\}, \\forall R:\\, \\alpha \\to \\alpha \\to \\mathrm{Prop}, \\forall x y:\\, \\alpha, (\\forall z, R\\ x\\ z \\to R\\ y\\ z) \\rightarrow \\forall l:\\, \\text{List }\\alpha,\\ IsChain\\, R\\, (x :: l) \\rightarrow \\ IsChain\\, R\\, (y :: l) $$$
Lean4
theorem imp_head {x y} (h : ∀ {z}, R x z → R y z) {l} (hl : IsChain R (x :: l)) : IsChain R (y :: l) :=
IsChain.cons_of_imp_of_cons (@h) hl
