Perm.merge_by: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/perm.bend as Perm
Lines 130-138 of bend-mathlib@0.8.1.0/perm.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/perm.bend&start_line=130&end_line=138

import Base

# Merges two lists, taking the head of xs first whenever le(x, y) holds.
def merge_by(~A: Data, ~le: A -> A -> Bool, xs: List<&2, A>, ys: List<&2, A>) -> List<&2, A>:
  match xs ys:
    case Nil{} _:
      ys
    case +x <> +xt Nil{}:
      x <> xt
    case +x <> +xt +y <> +yt:
      Bool.pick(List<&2, A>, le(x, y), x <> merge_by(~A, ~le, xt, y <> yt), y <> merge_by(~A, ~le, x <> xt, yt))

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List