Bytes.rgo: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend as Bytes
Lines 35-45 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&start_line=35&end_line=45

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR

# reverse.go(xs, ys) = reverse(xs) ++ ys
def rgo(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {List.reverse.go(&2, U32, xs, ys) == SCR.append(rev(xs), ys) : List<&2, U32>}:
  match xs:
    case Nil{}:
      {==}
    case Con{+h, +t}:
      Equal.trans(List<&2, U32>, List.reverse.go(&2, U32, t, Con{h, ys}), SCR.append(rev(t), Con{h, ys}), SCR.append(List.reverse.go(&2, U32, t, [h]), ys),
        rgo(t, Con{h, ys}),
        Equal.trans(List<&2, U32>, SCR.append(rev(t), Con{h, ys}), SCR.append(SCR.append(rev(t), [h]), ys), SCR.append(List.reverse.go(&2, U32, t, [h]), ys),
          Equal.sym(List<&2, U32>, SCR.append(SCR.append(rev(t), [h]), ys), SCR.append(rev(t), SCR.append([h], ys)), app_assoc(rev(t), [h], ys)),
          Equal.cong(List<&2, U32>, List<&2, U32>, l => SCR.append(l, ys), SCR.append(rev(t), [h]), List.reverse.go(&2, U32, t, [h]), Equal.sym(List<&2, U32>, List.reverse.go(&2, U32, t, [h]), SCR.append(rev(t), [h]), rgo(t, [h])))))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=List.reverse.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=app_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=rev
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend&name=append