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

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

# Moving an element from the middle to the front is a permutation.
def perm_move(-A: Data, +xs: List<&2, A>, +y: A, +t: List<&2, A>) -> K.perm(A, List.append(&2, A, xs, y <> t), y <> List.append(&2, A, xs, t)):
  match xs:
    case Nil{}:
      perm_refl(A, y <> t)
    case +x <> r:
      perm_trans(A, x <> List.append(&2, A, r, y <> t), x <> y <> List.append(&2, A, r, t), y <> x <> List.append(&2, A, r, t), perm_cons(A, x, List.append(&2, A, r, y <> t), y <> List.append(&2, A, r, t), perm_move(A, r, y, t)), perm_swap(A, x, y, List.append(&2, A, r, t)))

Uses (7):
  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=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=bend-mathlib@0.8.1.0/perm.bend&name=perm_swap
  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