English
If every p-application implies q, then a triplewise p-l list also triplewise q.
Русский
Если для всех a,b,c выполнение p a b c ⇒ q a b c, тогда l.Triplewise p ⇒ l.Triplewise q.
LaTeX
$$$$ (h : \\forall {a b c}, p a b c \\Rightarrow q a b c) \\rightarrow (hl : l.Triplewise p) \\Rightarrow l.Triplewise q. $$$$
Lean4
theorem imp (h : ∀ {a b c}, p a b c → q a b c) (hl : l.Triplewise p) : l.Triplewise q := by
induction hl with
| nil => exact .nil
| cons head tail ih => exact .cons (head.imp h) ih