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