Shuffle.go_occ: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/shuffle.bend as Shuffle
Lines 105-112 of bend-collections-laws-math@1.0.0.0/proofs/math/random/shuffle.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/shuffle.bend&start_line=105&end_line=112

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend as R

def go_occ(~A: Data, ~V: Data, ~rel: A -> V -> Bool, ~S: Data, ~next: S -> W.U64 & S, +v: V, +k: Nat, +n: W.U64, st: List<&2, A> & S) -> {occ(~A, ~V, ~rel, v, R.fst(List<&2, A>, S, R.shuffle_go(~A, ~S, ~next, k, n, st))) == occ(~A, ~V, ~rel, v, R.fst(List<&2, A>, S, st)) : Nat}:
  match k st:
    case 0n Tuple{+xs, +s}:
      {==}
    case 1n+p Tuple{+xs, +s}:
      Equal.trans(Nat, occ(~A, ~V, ~rel, v, R.fst(List<&2, A>, S, R.shuffle_go(~A, ~S, ~next, p, X.sub(n, W.U64{1, 0}), R.shuffle_step(~A, ~S, ~next, 1n+p, n, (xs, s))))), occ(~A, ~V, ~rel, v, R.fst(List<&2, A>, S, R.shuffle_step(~A, ~S, ~next, 1n+p, n, (xs, s)))), occ(~A, ~V, ~rel, v, xs),
        go_occ(~A, ~V, ~rel, ~S, ~next, v, p, X.sub(n, W.U64{1, 0}), R.shuffle_step(~A, ~S, ~next, 1n+p, n, (xs, s))),
        swap_at_occ(~A, ~V, ~rel, S, v, xs, 1n+p, R.uint64n(~S, ~next, s, n)))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/shuffle.bend&name=occ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/shuffle.bend&name=swap_at_occ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend&name=fst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend&name=shuffle_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend&name=shuffle_step
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend&name=uint64n
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=sub