Perm.merge_by_perm: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/perm.bend as Perm
Lines 147-155 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=147&end_line=155

import Base
import bendlib-kernel-list@1.0.0.0/list.bend as K

# Merging permutes the concatenation.
def merge_by_perm(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>, +ys: List<&2, A>) -> K.perm(A, List.append(&2, A, xs, ys), merge_by(~A, ~le, xs, ys)):
  match xs ys:
    case Nil{} _:
      perm_refl(A, ys)
    case +x <> +xt Nil{}:
      perm_cons(A, x, List.append(&2, A, xt, Nil{}), xt, perm_append_nil(A, xt))
    case +x <> +xt +y <> +yt:
      internal_merge_pick(A, le(x, y), x, xt, y, yt, merge_by(~A, ~le, xt, y <> yt), merge_by(~A, ~le, x <> xt, yt), merge_by_perm(~A, ~le, xt, y <> yt), merge_by_perm(~A, ~le, x <> xt, yt))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=internal_merge_pick
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=merge_by
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=perm_append_nil
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=perm_cons
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=perm_refl
  https://jend.leeeet.dev/definition.txt?path=bendlib-kernel-list@1.0.0.0/list.bend&name=perm