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

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

def internal_sym_eq(-A: Data, +s: List<&2, Nat>, +xs: List<&2, A>, -ys: List<&2, A>, e: K.perm_steps(A, s, xs, ys)) -> K.perm_steps(A, internal_invert(s), ys, xs):
  %e : {K.apply(A, internal_invert(s), _) == xs : List<&2, A>}
  internal_apply_invert(A, s, xs)

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=internal_apply_invert
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=internal_invert
  https://jend.leeeet.dev/definition.txt?path=bendlib-kernel-list@1.0.0.0/list.bend&name=apply
  https://jend.leeeet.dev/definition.txt?path=bendlib-kernel-list@1.0.0.0/list.bend&name=perm_steps