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

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

# Splitting into evens and odds is a permutation.
def split_perm(-A: Data, +xs: List<&2, A>) -> K.perm(A, xs, List.append(&2, A, evens(A, xs), odds(A, xs))):
  match xs:
    case Nil{}:
      perm_refl(A, Nil{})
    case +x <> r:
      match r:
        case Nil{}:
          perm_refl(A, x <> Nil{})
        case +y <> t:
          perm_cons(A, x, y <> t, List.append(&2, A, evens(A, t), y <> odds(A, t)), perm_trans(A, y <> t, y <> List.append(&2, A, evens(A, t), odds(A, t)), List.append(&2, A, evens(A, t), y <> odds(A, t)), perm_cons(A, y, t, List.append(&2, A, evens(A, t), odds(A, t)), split_perm(A, t)), perm_move_rev(A, evens(A, t), y, odds(A, t))))

Uses (9):
  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=evens
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=odds
  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_move_rev
  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=bend-mathlib@0.8.1.0/perm.bend&name=perm_trans
  https://jend.leeeet.dev/definition.txt?path=bendlib-kernel-list@1.0.0.0/list.bend&name=perm