∀ {α : Type u_1} {p : α → α → α → Prop} {motive : (a : List α) → List.Triplewise p a → Prop},
  motive [] ⋯ →
    (∀ {a : α} {l : List α} (a_1 : List.Pairwise (p a) l) (a_2 : List.Triplewise p l),
        motive l a_2 → motive (a :: l) ⋯) →
      ∀ {a : List α} (t : List.Triplewise p a), motive a t