English
Adding an element to the front of a list relates its triplewise property to the triplewise of the tail and the pairwise of the tail with p(a, ·).
Русский
Добавление элемента вперед списка связывает его свойство triplewise с тройной последовательностью хвоста и попарностью хвоста относительно p a.
LaTeX
$$$$ (a :: l).Triplewise\\, p \\iff l.Pairwise\\,(p\\,a) \\land l.Triplewise\\, p. $$$$
Lean4
@[grind =]
theorem triplewise_cons : (a :: l).Triplewise p ↔ l.Pairwise (p a) ∧ l.Triplewise p := by rw [triplewise_iff]; aesop