∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → α → α → Prop},
  List.Triplewise p (l₁ ++ l₂) =
    (List.Triplewise p l₁ ∧
      List.Triplewise p l₂ ∧ (∀ a ∈ l₁, List.Pairwise (p a) l₂) ∧ ∀ a ∈ l₂, List.Pairwise (fun x y => p x y a) l₁)