English
Reversing a list converts triplewise p to triplewise with p reversed: l.reverse is triplewise under p' if l is triplewise under p, where p'(a,b,c) := p c b a.
Русский
Обращение списка превращает тройственность: если l тройственно относительно p, то l.reverse тройственно относительно p' с p'(a,b,c) := p(c,b,a).
LaTeX
$$$l.\text{Triplewise } p \iff l.\text{Triplewise } (\\lambda a\,b\,c, p\, c\, b\, a)$$$
Lean4
theorem triplewise_reverse : l.reverse.Triplewise p ↔ l.Triplewise fun a b c ↦ p c b a := by
induction l with
| nil => simp
| cons h t ih => simp [triplewise_append, pairwise_reverse, triplewise_cons, ih, and_comm]