∀ {α : Type u_1} {le : α → α → Bool},
  (∀ (a b c : α), le a b = true → le b c = true → le a c = true) →
    (∀ (a b : α), (le a b || le b a) = true) →
      ∀ (l₁ l₂ : List α),
        List.Pairwise (fun a b => le a b = true) l₁ →
          List.Pairwise (fun a b => le a b = true) l₂ → List.Pairwise (fun a b => le a b = true) (l₁.merge l₂ le)