Proof.Random.shuffle: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/proof.bend as Proof
Lines 69-70 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/proof.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/proof.bend&start_line=69&end_line=70

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend as CR
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/shuffle.bend as SH

def Random.shuffle(~A: Data, ~V: Data, ~rel: A -> V -> Bool, +g: CR.Gen, +items: List<&2, A>, +v: V) -> SCR.Random.shuffle(~A, ~V, ~rel, g, items, v):
  SH.shuffle_perm(~A, ~V, ~rel, ~CR.Gen, ~CR.next, g, items, v)

Uses (6):
  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=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/shuffle.bend&name=shuffle_perm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend&name=Random.shuffle
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend&name=Gen
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend&name=next