∀ {α : Type u_1} (xs ys : List α) (le : α → α → Bool),
  xs.merge ys le =
    match xs, ys with
    | [], ys => ys
    | xs, [] => xs
    | x :: xs, y :: ys => if le x y = true then x :: xs.merge (y :: ys) le else y :: (x :: xs).merge ys le