English
If R is transitive, R(hd, tl_hd) holds, and the tail (tl_hd, tl_tl) is pairwise under R, then the whole 3-element sequence (hd, tl_hd, tl_tl) is pairwise under R.
Русский
Если R.transitive, и R(hd, tl_hd) выполняется, и хвост (tl_hd, tl_tl) попарно связанно по R, то вся последовательность hd, tl_hd, tl_tl попарно связана по R.
LaTeX
$$$[IsTrans\\ R] \\land R(hd, tl\\_hd) \\land \\operatorname{Pairwise}(R, \\mathrm{cons}(tl\\_hd, tl\\_tl)) \\Rightarrow \\operatorname{Pairwise}(R, \\mathrm{cons}(hd, \\mathrm{cons}(tl\\_hd, tl\\_tl)))$$$
Lean4
theorem cons_cons_of_trans {R : α → α → Prop} [IsTrans _ R] {hd tl_hd : α} {tl_tl : Seq α} (h_hd : R hd tl_hd)
(h_tl : Pairwise R (.cons tl_hd tl_tl)) : Pairwise R (.cons hd (.cons tl_hd tl_tl)) :=
by
apply Pairwise.cons _ h_tl
simp only [mem_cons_iff, forall_eq_or_imp]
exact ⟨h_hd, fun x hx ↦ Trans.simple h_hd ((cons_elim h_tl).left x hx)⟩
