law take_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/stream.bend:198

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R

198law take_eq:
199  for +n: Nat
200  for +xs: List<&2, U32>
201  {I.take(n, xs) == R.prefix(n, xs) : List<&2, U32>}